汽车安全巡航控制系统的设计与验证

鉴于近期全球人口的巨大增长，车辆数量也出现了庞大且不受控制的增长，从而在很大程度上增加了道路事故的数量。作为上述问题的一种解决方案，我们的系统尝试使用同步编程语言来缓解这一问题。目标是开发一个安全碰撞预警系统，该系统将处理追尾碰撞，并在威胁达到非常高的水平时接管对车辆的控制。根据环境条件进行适配也是该系统的一个突出特点。安全系统向驾驶员提供警告，以协助避免与其他车辆发生追尾碰撞。最初，系统提供低级别警报，随着威胁严重程度的增加，警告或警报的级别也随之提高。在最高威胁级别，系统进入巡航控制模式，此时系统通过控制发动机节气门以及（如果允许的话）车辆的制动系统来控制车辆的速度。我们关注这一碰撞区域，因为它占碰撞相关死亡人数的比例非常高。为了证明系统的可行性、鲁棒性和可靠性，我们还使用时序逻辑以及一个在 ESTEREL 中的参考实现证明了系统的某些属性。为支持这一点，我们形式化地验证了系统的各种属性及其证明。