软件学报

作者：陆芝浩，王瑞，孔辉，关永，施智平

单位：陆芝浩，首都师范大学 信息工程学院, 北京 100048;轻型工业机器人与安全验证北京市重点实验室(首都师范大学), 北京 10004811,王瑞，首都师范大学 信息工程学院, 北京 100048;轻型工业机器人与安全验证北京市重点实验室(首都师范大学), 北京 10004802,孔辉，华为技术上海研发中心, 上海 20120603,关永，首都师范大学 信息工程学院, 北京 100048;电子系统可靠性与数理交叉学科国家国际科技合作示范基地(首都师范大学), 北京 10004804,施智平，首都师范大学 信息工程学院, 北京 100048;轻型工业机器人与安全验证北京市重点实验室(首都师范大学), 北京 10004805

关键词：形式化验证;Ptolemy离散事件模型;模型自动转换;时间自动机

基金：国家自然科学基金（61877040，61876111）；首都师范大学交叉研究院项目（19530012005）

Ptolemy是一个广泛应用于信息物理融合系统的建模和仿真工具包，主要通过仿真的方式保证所建模型的正确性.形式化方法是保证系统正确性的重要方法之一.提出了一种基于形式模型转换的方法来验证离散事件模型的正确性.离散事件模型根据不同事件的时间戳触发组件，时间自动机模型能够表达这个特征，因此选用Uppaal作为验证工具.首先定义了离散事件模型的形式语义；其次设计了一组从离散事件模型到时间自动机的映射规则；然后在Ptolemy环境中实现了一个插件，可以自动将离散事件模型转换为时间自动机模型，并通过调用Uppaal验证内核完成验证；最后，以一个交通信号灯控制系统为例进行了成功的转换和验证，实验结果证实了该方法能够验证Ptolemy离散事件模型的正确性.

来源：2021年第6期

《软件学报》期刊编辑部

查看软件学报杂志2021年第6期