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

Formal Verification of Ptolemy Discrete Event Model

作　　者：陆芝浩 王瑞[1,2] 孔辉 关永[1,4] 施智平[1,2] LU Zhi-Hao;WANG Rui;KONG Hui;GUAN Yong;SHI Zhi-Ping(College of Information Engineering,Capital Normal University,Beijing 100048,China;Beijing Key Laboratory of Light Industrial Robot and Safety Verification(Capital Normal University),Beijing 100048,China;Huawei Technologies Shanghai R&D Center,Shanghai 201206,China;National International Science and Technology Cooperation Demonstration Base of Interdisciplinary of Electronic System Reliability and Mathematics(Capital Normal University),Beijing 100048,China)

机构地区：[1]首都师范大学信息工程学院,北京100048 [2]轻型工业机器人与安全验证北京市重点实验室(首都师范大学),北京100048 [3]华为技术上海研发中心,上海201206 [4]电子系统可靠性与数理交叉学科国家国际科技合作示范基地(首都师范大学),北京100048

出　　处：《软件学报》2021年第6期1830-1848,共19页Journal of Software

基　　金：国家自然科学基金(61877040,61876111);首都师范大学交叉研究院项目(19530012005)。

摘　　要：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.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 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 the proposed approach is reliable and effective for the verification of Ptolemy discrete event model.

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]