Formal Verification of Ptolemy Discrete Event Model

被引：0
|
作者：
Lu Z.-H. [1 ,2 ]
Wang R. [1 ,2 ]
Kong H. [3 ]
Guan Y. [1 ,4 ]
Shi Z.-P. [1 ,2 ]
机构：
[1] College of Information Engineering, Capital Normal University, Beijing
[2] Beijing Key Laboratory of Light Industrial Robot and Safety Verification, Capital Normal University, Beijing
[3] Huawei Technologies Shanghai R&D Center, Shanghai
[4] National International Science and Technology Cooperation Demonstration Base of Interdisciplinary of Electronic System Reliability and Mathematics, Capital Normal University, Beijing
来源：
Wang, Rui (rwang04@cnu.edu.cn) | 1830年 / Chinese Academy of Sciences卷 / 32期
基金：
中国国家自然科学基金;
关键词：
Automatic model translation; Formal verification; Ptolemy DE model; Timed automata;
D O I：
10.13328/j.cnki.jos.006252
中图分类号：
学科分类号：
摘要：
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. © Copyright 2021, Institute of Software, the Chinese Academy of Sciences. All rights reserved.
引用
收藏
页码：1830 / 1848
页数：18
相关论文
共 23 条
  • [1] Joseph B, Soonho H, Edward L, David M., Ptolemy: A framework for simulating and prototyping heterogeneous systems, Int'l Journal of Computer Simulation, 10, (1995)
  • [2] Wang J, Zhan NJ, Feng XY, Liu ZM., Overview of formal methods, Ruan Jian Xue Bao/Journal of Software, 30, 1, pp. 33-61, (2019)
  • [3] Lin HM, Zhang WH., Model checking: Theories, techniques and applications, Acta Electronica Sinica, 30, z1, pp. 1907-1912, (2002)
  • [4] Mudit G, Kienhuis B, Edward L, Liu J., Ptolemy II-Heterogeneous Concurrent Modeling and Design in Java, (1999)
  • [5] Alur R, Dill DL., A theory of timed automata, Theoretical Computer Science, 126, 2, pp. 183-235, (1994)
  • [6] Behrmann G, David A, Larsen K., A tutorial on uppaal, Proc. of the Formal Methods for the Design of Real-Time Systems, pp. 200-236, (2004)
  • [7] Bengtsson J, Yi W., Timed automata: Semantics, algorithms and tools, LNCS, pp. 87-124, (2003)
  • [8] Xing JS, Theelen BD, Langerak R, Van JDP, Tretmans J, Voeten JPM., From POOSL to UPPAAL: Transformation and quantitative analysis, Proc. of the 2010 10th Int'l Conf. on Application of Concurrency to System Design, pp. 47-56, (2010)
  • [9] Guo C, Ren SP, Jiang Y, Wu PL, Sha L, Richard B, Berlin J., Transforming medical best practice guidelines to executable and verifiable statechart models, Proc. of the ACM/IEEE Int'l Conf. on Cyber-Physical Systems, (2016)
  • [10] Jiang Y, Liu H, Song H, Kong H, Wang R, Guan Y, Liu S., Safety-Assured model-driven design of the multifunction vehicle bus controller, IEEE Trans. on Intelligent Transportation Systems, 19, 10, (2018)
123