基于贝叶斯网络构建RoboSim模型的自动驾驶行为决策

为汽车自动驾驶提供安全高效的自动驾驶行为决策,是汽车自动驾驶领域面临的挑战性问题之一.目前,随着自动驾驶行业的蓬勃发展,工业界与学术界提出了诸多自动驾驶行为决策方法,但由于汽车自动驾驶行为决策受环境不确定因素的影响,决策本身也要求实效性及高安全性,现有的行为决策方法难以完全支撑这些要素.针对以上问题,提出了一种基于贝叶斯网络构建RoboSim模型的自动驾驶行为决策方法.首先,基于领域本体分析自动驾驶场景元素之间的语义关系,并结合LSTM模型预测场景中动态实体的意图,进而为构建贝叶斯网络提供驾驶场景理解信息;然后,通过贝叶斯网络推理特定场景的自动驾驶行为决策,并使用RoboSim模型的状态迁移承载行为决策的动态执行过程,以减少贝叶斯网络推理的冗余操作,提高了决策生成的效率. RoboSim模型具有平台无关、能模拟仿真执行周期的特点,并支持多种形式化的验证技术.为确保行为决策的安全性,使用模型检测工具UPPAAL对RoboSim模型进行验证分析.最后,结合变道超车场景案例,进一步证实所提方法的可行性,为设计安全、高效的自动驾驶行为决策提供了一种可行的途径.     

设备自动巡检控制逻辑的层级时间自动机建模与验证

地下建筑工程中的设备系统经常处于静止状态,为保证其在需要时能安全可靠地运行,需对设备进行定期的自动巡检。在自动巡检的过程中,设备自动巡检控制逻辑起到了举足轻重的作用。为了解决复杂的设备自动巡检控制逻辑造成的一系列问题,之前提出了一种层级有限自动机(HFA)的形式化模型,并利用HFA对设备自动巡检控制逻辑实现了行为建模,但并未添加时间属性,也未验证其正确性与可靠性。现提出一种层级时间自动机形式化模型,并利用它对设备自动巡检控制逻辑进行建模,再利用UPPAAL对其进行分析与形式化验证,分别验证其安全性、可达性、活性及时间约束,以此来确保其时效正确性与可靠性。这种建模与形式化验证方法弥补了之前无时间约束的漏洞,有效确保了设备自动巡检控制逻辑的正确性与可靠性。最终,该模型通过了模拟和验证,这充分证明了设备自动巡检控制逻辑是正确可靠的。     

基于观察者模式的实时系统验证方法

复杂实时系统的验证问题一直备受关注。验证过程中,验证特性可以用时序逻辑来描述,但时序逻辑对于非专业人员而言较为复杂,难度较大。观察者模式是一个额外的子系统,可以将复杂的验证特性转换为简单的可达性问题,同时也可以避免使用复杂的验证算法。将Etienne和Nouha Abid等人提出的抽象的观察者模式应用到实时系统实例——Train-Gate系统中,采用UPPAAL工具对Train-Gate系统中的某些场景建立观察者模型,并采用对比实验将验证结果与无观察者模式状态下的验证结果进行对比。对比结果表明,使用观察者模式和验证特性都可以得到正确的验证结果,但观察者更节省时间,对于非专业人员而言更简单且更容易接受。因此,使用观察者模式对如Train-Gate的实时系统进行验证是可行的。     

Formal verification of a radio network random access protocol

In this paper, the random access procedure of Universal Mobile Telecommunications System network is investigated. We have proposed a model based on communicating timed automata that represents the main functions related to the random access procedure including the user equipment, the base station (node B or BTS), and the channel. Then, we have used computational tree logic formula to specify the proprieties to be verified. The model and the formulas serve as inputs to the model checker, which is used as a verification engine, ie, UPPAAL and SPIN. The formal verification approach shows that the protocol has several drawbacks that may not be detected by simulation.     

不可靠环境下多轮FR协议分析

随着网络的大规模应用,越来越多的协议在并发的、不可靠的环境中执行。文章用有限自动机对FR协议建模,并用自动验证工具UPPAAL验证了多轮协议在可靠环境下的性质。重点验证了不可靠环境中多轮协议的执行情况,最后对协议进行了修改。     

A Ravenscar-Compliant Run-time Kernel for Safety-Critical Systems*

The Ravenscar tasking profile for Ada 95 has been designed to allow implementation of highly safety critical systems. Ravenscar defines a tasking system with deterministic behavior and low complexity. We provide a formal model using UPPAAL of the primitives provided by Ravenscar including exceptions. This formal model is used to verify the correctness of the Ravenscar model and can be used to verify safety properties of applications using the Ravenscar profile. As an illustration of this, we model a sample application using all features of Ravenscar and formally verify its correctness. Furthermore, an introduction to the Ravenscar model is given.     

基于UPPAAL的实时系统模型验证

UPPAAL是一种使用时间自动机模型的实时系统验证工具，它可以避免时间自动机求积时状态空间的爆炸。介绍了时间自动机理论和工具UPPAAL，着重说明如何用UPPAAL进行模型检查，并给出了一个应用实例。     

基于时间自动机的道岔自动控制研究

实时系统由于受时间约束,设计和验证具有很高的挑战性。用多个时间自动机来规范模拟道岔自动控制系统,给出了一种自动化的道岔控制模型(TTCQ),并采用UPPAAL作为模型验证工具,证明了该模型具有安全性、有效性和可控性。所采用的方法避免了积的等价类状态空间的爆炸,减少了验证的搜索空间,为铁路交通提供了一种可行的、安全的、智能的控制机制。     

基于模型的车载设备测试用例自动生成研究

针对人工生成测试序列的不足,提出基于模型的车载设备测试用例自动生成方法。首先按照系统需求规范,在UPPAAL环境下运用时间自动机对车载设备进行建模及验证,然后将建立的模型导入到基于覆盖度算法的模型辅助工具Cover中自动生成测试用例,最后分析了自动生成的测试用例的正确性。       

基于实体交互模型巷道瓦斯监测WSNs的可用性检验

若煤矿瓦斯监测WSNs(Wireless Sensor Networks)系统的功能设计忽略了被监测实体的交互行为,会造成WSNs本身可靠而被监测实体的安全不满足情况,这在生产安全中是非常危险的。为检验WSNs监测系统功能设计的可靠性和可用性,利用时间自动机模型检验方法建立WSNs监测系统模型,检验WSNs系统的可靠性。然后,根据传感器与环境实体间的交互关系,分析煤矿中多个实体的并发行为,提出了监测WSNs与被监测实体交互并发行为的时间自动机模型和可用性性质描述的建立方法,从监测功能设计角度,将被监测实体的安全并入WSNs监测生产安全的功能性质,然后用模型检验方法进行机器检验,保障了监测系统的可用性。对含有并发结构的实体模型,利用分支行为等价构建并发时间自动机模型,再利用实体间的并发分支汇聚行为互模拟的方法,进行了并发行为模型的状态约减,并通过互模拟等价证明了该方法的正确性。状态约减前后的实验对比表明该方法提高了检验效率。最后,对现行巷道中瓦斯传感器的部署标准,利用该方法对其中的实际部署方案进行建模并检验,在模型中考虑实体的并发行为,发现在并发事件发生时,其中一个含支巷的瓦斯部署模型存在一个潜在的瓦斯泄露漏检问题。利用实体建模的模型检验方法需要建立自动建模机制,以提高该方法的实用性。