基于实时UML顺序图的物联网交互模型

物联网是一个集计算、通信和控制于一体的智能系统,它通过监控和收集物理进程信息并将这些信息进行计算和分析,最终生成正确的控制指令用以执行,从而使物理环境变得更加安全和可靠。在物联网中,各物体通过网络连接或者本地连接的方式进行交互,这些交互具有时间性和地域性。物联网的建模和验证是物联网研究中一个重要的领域。文中提出一种基于实时UML顺序图的物联网交互模型,该模型将物联网中所有参与交互的物体建模为交互对象,并且通过实时UML顺序图对交互对象间的交互进行建模。使用时间自动机对交互对象的内部状态变化进行建模,以形成对交互模型的补充。最后根据转换规则将交互模型转换为时间自动机的形式以便于验证。通过一个实例,显示了如何具体应用物联网交互模型。进一步提出了物联网系统应该满足的一些性质,并使用UPPAAL模型检测工具对物联网交互模型进行分析和验证。

基于Timed-UML顺序图的RBC交接形式化建模与分析

在CTCS-3级列控系统中,采用RBC技术将线路划分成多个管辖区段。当列车行驶并跨越相邻RBC交界区域时,控制权将会移交至前方相邻RBC,整个过程称为RBC交接。在运行中,RBC交接过程能否实时安全可靠地执行,直接影响着列车的行车效率和乘客的生命安全。采用一种基于添加实时约束的UML顺序图与时间自动机结合的模型来建立RBC交接场景。以双车载电台的RBC切换策略出发,建立切换的Timed-UML顺序图模型,然后按照UML-TA转换规则,建立得到完整的时间自动机网络模型。并利用UPPAAL验证工具对RBC交接模型进行形式化建模及分析,对模型的死锁和功能实现做了验证,从而达到对CTCS-3级RBC子系统的实时性以及设计规范合理性的验证目的。