摘要：轨道交通区域控制器对行车安全至关重要,设备投入使用前需进行严格的测试,针对目前区域控制器测试序列人工生成,测试效率低的问题,提出一种基于时间自动机模型的测试序列自动生成方法。首先分析区域控制器的功能建立时间自动机模型,用UPPAAL对模型的正确性进行验证;编写MFC应用程序,利用Tiny XML解析库解析模型文件,提取状态信息和变迁条件,生成测试案例集;由测试功能划分测试序列的初始状态和结束状态,并根据测试案例的串接条件,利用深度优先搜索设计最小重复度算法将测试案例串接成测试序列;最后,利用该方法生成了区域控制器切换功能的测试序列,通过分析可知生成的测试序列符合区域控制器的工作流程和测试环境,结果证明该方法能有效提高测试序列的生成效率。

摘要：采用时间自动机形式化模型检验方法建立了结构分析与设计语言(AADL)调度模型的自动机,实现了从AADL模型到时间自动机模型的自动转换与验证.首先,设计了周期、非周期的线程时间自动机模板及抢占、非可抢占的调度器时间自动机模板,建立了AADL调度模型到时间自动机模型的语义映射法则.然后,设计了自动化模型转换插件,并将其集成到OSATE建模工具中,实现了建模、转换、验证的集成开发环境.最后,利用UPPAAL工具对时间自动机模型进行模拟与验证.仿真实验结果表明,所建立的模型转换方法能够有效、实时地将AADL模型转换为时间自动机模型,并可在UPPAAL中分析原模型的可调度性.

摘要：为对系统功能需求进行可视化仿真和验证,在对UML可视化建模工具Enterprise Architect中时序图模型的组成图形元素,以及可视化仿真与验证工具UPPAAL中时间自动机模型的组成图形元素进行深入分析后,对现有的时序图到时间自动机模型的转换算法进行改进并提出更加完善的算法,对转换后的时间自动机布局算法进行相关研究,实现从时序图模型到时间自动机模型的自动转换与布局。在实际领域的实验结果表明,改进后的算法能够对系统功能需求进行正确有效的可视化验证和仿真,提高了系统模型设计效率。

摘要：为了克服传统信号灯控制模式下交叉口物理空间使用效率不高的问题,提出一种基于时间自动机的无信号灯交叉路口交通管理模型。将交叉口划分为互不相交的物理空间路权资源,采用时间自动机模型描述每辆到达车辆通过交叉口的动态过程,并在此基础上将交叉口内所有车辆的时间自动模型耦合在一起生成系统模型,在考虑安全性的前提下设计最大化交叉口通行效率的车辆调度策略。实验结果表明,较传统交叉口有信号控制方式,基于时间自动机模型的无信号交叉口控制方法更加充分地利用了交叉路口的物理空间,交叉口的车辆吞吐能力得到进一步提升。

摘要：体系结构分析设计语言AADL是一种可支持软硬件一体化建模及同一模型多元分析的形式化与图形化建模语言。采用时间自动机形式化模型检验方法对AADL模型中的数据流进行转换和验证。考虑到单一数据流与混合数据流的差异性,分别设计了数据流到时间自动机模型的转换规则,并通过时间自动机网络实现数据流的综合分析。设计开发了自动化模型转换的插件AADLToUppaal Plug-in,将其嵌入到OSTATE工具中,使用时间自动机建模与验证工具Uppaal对转换得到的时间自动机进行模拟和验证,等价地验证所设计的AADL模型数据流时延是否满足系统实时性要求。仿真实验结果表明,所设计的数据流模型转换方法能有效地将AADL模型转换到时间自动机模型,并能在Uppaal中正确地分析原模型的数据流时延特性。