| 陆芝浩,王瑞,孔辉,关永,施智平.Ptolemy离散事件模型形式化验证方法.软件学报,2021,32(6):27-0 |
| Ptolemy离散事件模型形式化验证方法 |
| Formal Verification of Ptolemy Discrete Event Model |
| 投稿时间：2020-08-30 修订日期：2020-10-26 |
| DOI：10.13328/j.cnki.jos.006252 |
| 中文关键词: 形式化验证 Ptolemy离散事件模型 模型自动转换 时间自动机 |
| 英文关键词:formal verification Ptolemy DE model automatic model translation timed automata |
| 基金项目:国家自然科学基金（61877040，61876111）；首都师范大学交叉研究院项目（19530012005） |
|
| 摘要点击次数: 54 |
| 全文下载次数: 25 |
| 中文摘要: |
| Ptolemy是一个广泛应用于信息物理融合系统的建模和仿真工具包，主要通过仿真的方式保证所建模型的正确性.形式化方法是保证系统正确性的重要方法之一.本文提出了一种基于形式模型转换的方法来验证离散事件模型的正确性.离散事件模型根据不同事件的时间戳触发组件，时间自动机模型能够表达这个特征，因此选用Uppaal作为验证工具.首先定义了离散事件模型的形式语义，其次设计了一组从离散事件模型到时间自动机的映射规则.然后在Ptolemy环境中实现了一个插件，可以自动将离散事件模型转换为时间自动机模型，并通过调用Uppaal验证内核完成验证.最后以一个交通信号灯控制系统为例进行了成功的转换和验证，实验结果证实了该方法能够验证Ptolemy离散事件模型的正确性. |
| 英文摘要: |
| 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. In this paper, we present 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 of timed automata. Then, a plug-in is implemented in the Ptolemy environment that automatically translated the discrete event model into a network of timed automata, and verifies the network of timed automata by calling the Uppaal validation kernel. Finally, a case of traffic light control system is successfully translated and verified, and the experimental results confirm that our approach is reliable and effective for the verification of Ptolemy discrete event model. |
|
HTML 下载PDF全文 查看/发表评论 下载PDF阅读器 |
