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

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

Formal Verification of Ptolemy Discrete Event Model

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.