Page 256 - 《软件学报》2021年第6期

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
Journal of Software,2021,32(6):1830−1848 [doi: 10.13328/j.cnki.jos.006252] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

∗
Ptolemy 离散事件模型形式化验证方法

1,2
1,4
1,2
3
陆芝浩 , 王 瑞 , 孔 辉 , 关 永 , 施智平 1,2
1
(首都师范大学 信息工程学院,北京 100048)
2 (轻型工业机器人与安全验证北京市重点实验室(首都师范大学),北京 100048)
3 (华为技术上海研发中心,上海 201206)
4
(电子系统可靠性与数理交叉学科国家国际科技合作示范基地(首都师范大学),北京 100048)
通讯作者: 王瑞, E-mail: rwang04@cnu.edu.cn

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

中文引用格式: 陆芝浩,王瑞,孔辉,关永,施智平.Ptolemy 离散事件模型形式化验证方法.软件学报,2021,32(6):1830−1848.
http://www.jos.org.cn/1000-9825/6252.htm
英文引用格式: Lu ZH, Wang R, Kong H, Guan Y, Shi ZP. Formal verification of Ptolemy discrete event model. Ruan Jian Xue
Bao/Journal of Software, 2021,32(6):1830−1848 (in Chinese). http://www.jos.org.cn/1000-9825/6252.htm
Formal Verification of Ptolemy Discrete Event Model

1,2
1,2
1,4
3
LU Zhi-Hao , WANG Rui , KONG Hui , GUAN Yong , SHI Zhi-Ping 1,2
1
(College of Information Engineering, Capital Normal University, Beijing 100048, China)
2
(Beijing Key Laboratory of Light Industrial Robot and Safety Verification (Capital Normal University), Beijing 100048, China)
3
(Huawei Technologies Shanghai R&D Center, Shanghai 201206, China)
4
(National International Science and Technology Cooperation Demonstration Base of Interdisciplinary of Electronic System Reliability
and Mathematics (Capital Normal University), Beijing 100048, China)
Abstract: Ptolemy is a modeling and simulation toolkit widely used in cyber physical systems, which ensures the correctness of the
models through simulation. Formal verification is one of the important methods to guarantee the correctness of systems. This paper
presents a model translation based approach to verify the Ptolemy discrete event model. The discrete event model fires according to the
timestamp of different events, and the timed automaton can express this feature. Therefore, Uppaal is a suitable verification tool. First, the
semantic of discrete event model is defined. And a set of mapping rules are designed to represent the discrete event model with a network

∗ 基金项目: 国家自然科学基金(61877040, 61876111); 首都师范大学交叉研究院项目(19530012005)
Foundation item: National Natural Science Foundation of China (61877040, 61876111); Cross Research Institute of Capital Normal
University (19530012005)
本文由“形式化方法与应用”专题特约编辑姜宇副教授推荐.
收稿时间: 2020-08-30; 修改时间: 2020-10-26; 采用时间: 2020-12-19; jos 在线出版时间: 2021-02-07