微信服务号

微信订阅号

2025-4-6- 9
Home > Archive>Volume 32, Issue 6, 2021 >1830-1848. DOI:10.13328/j.cnki.jos.006252
PDF HTML XML Export Cite reminder
Formal Verification of Ptolemy Discrete Event Model
Author:
Affiliation:

Fund Project:

National Natural Science Foundation of China (61877040, 61876111); Cross Research Institute of Capital Normal University (19530012005)

  • Article
    • | |
  • Metrics
    • |
  • Reference
    • |
  • Related
    • |
  • Cited by
    • | |
  • Comments
    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 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.

    Reference
    Related
    Cited by
Get Citation

陆芝浩,王瑞,孔辉,关永,施智平. Ptolemy离散事件模型形式化验证方法.软件学报,2021,32(6):1830-1848

Copy
Share
Article Metrics
  • Abstract:
  • PDF:
  • HTML:
  • Cited by:
History
  • Received:August 30,2020
  • Revised:October 26,2020
  • Online: February 07,2021
  • Published: June 06,2021
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the firstVisitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063