微信服务号

微信订阅号

2025-4-3- 23
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 [29]
    • |
  • Related
    • | | |
  • 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
    [1] Joseph B, Soonho H, Edward L, David M. Ptolemy:A framework for simulating and prototyping heterogeneous systems. Int'l Journal of Computer Simulation, 1995,10.
    [2] Wang J, Zhan NJ, Feng XY, Liu ZM. Overview of formal methods. Ruan Jian Xue Bao/Journal of Software, 2019,30(1):33-61(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5652.htm[doi:10.13328/j.cnki.jos.005652]
    [3] Lin HM, Zhang WH. Model checking:Theories, techniques and applications. Acta Electronica Sinica, 2002,30(z1):1907-1912(in Chinese with English abstract).
    [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, 1994,126(2):183-235.
    [6] Behrmann G, David A, Larsen K. A tutorial on uppaal. In:Proc. of the Formal Methods for the Design of Real-Time Systems. Springer, 2004. 200-236.
    [7] Bengtsson J, Yi W. Timed automata:Semantics, algorithms and tools. LNCS, 2003,87-124.
    [8] Xing JS, Theelen BD, Langerak R, Van JDP, Tretmans J, Voeten JPM. From POOSL to UPPAAL:Transformation and quantitative analysis. In:Proc. of the 201010th Int'l Conf. on Application of Concurrency to System Design. 2010. 47-56.[doi:10.1109/ACSD. 2010.21]
    [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. In:Proc. of the ACM/IEEE Int'l Conf. on Cyber-Physical Systems. ACM, 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, 2018,19(10).
    [11] Csertan G, Huszerl G, Majzik I, Pap Z, Andras P. VIATRA-Visual automated transformations for formal verification and validation of UML models. In:Proc. of the Automated Software Engineering. 2002. 267-270.[doi:10.1109/ASE.2002.1115027]
    [12] Jordi C, Robert C, Daniel R. UMLtoCSP:A tool for the formal verification of UML/OCL models using constraint programming. In:Proc. of the 22nd IEEE/ACM Int'l Conf. on Automated Software Engineering (ASE 2007). New York:Association for Computing Machinery, 2007. 547-548.[doi:https://doi.org/10.1145/1321631.1321737]
    [13] Liu Y, Ma ZY, He X, Shao WZ. Approach to transforming UML model to reliability analysis model. Ruan Jian Xue Bao/Journal of Software, 2010,21(2):287-304(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/3792.htm[doi:10.3724/SP.J. 1001.2010.03792]
    [14] Yang ZB, Hu K, Zhao YW, Ma DF, Bodeveix JP. Verification of AADL models with timed abstract state machines. Ruan Jian Xue Bao/Journal of Software, 2015,26(2):202-222(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/4776.htm[doi:10.13328/j.cnki.jos.004776]
    [15] Berthomieu B, Bodeveix JP, Chaudet C, Zilio SD, Filali M, Vernadat F. Formal verification of AADL specifications in the topcased environment. In:Proc. of the 14th Ada-Europe Int'l Conf. on Reliable Software Technologies. Berlin, Heidelberg:Springer-Verlag, 2009. 207-221.[doi:10.1007/978-3-642-01924-1_15]
    [16] Liang ML, Wang XP, Xue XP, Li G. Formal verification of UML models based on TLA. Computer Engineering, 2011,37(2):72-74.
    [17] Jiang Y, Song HB, Yang YX, Liu H, Gu M, Guan Y, Sun JG, Sha L. Dependable model-driven development of CPS:From stateflow simulation to verified implementation. ACM Trans. on Cyber-Physical Systems, 2019,3(1):12:1-12:31.
    [18] Hu K, Zhang T, Yang ZB, Gu B, Jiang S, Jiang BC. Formal verification of TASM models by translating into UPPAAL. Journal of Donghua University (English Edition), 2012,29(1):54-57.
    [19] Michael R, Strichman O. Translation validation:From simulink to C. In:Proc. of CAV 2009. 2009. 696-701.[doi:10.1007/978-3-642-02658-4_57]
    [20] Guo DQ, Lü JD, Wang SL, Tang T, Zhan NJ, Zhou DT. Formal analysis and verification of train control system of High-speed railway in China. Scientia Sinica Informationis, 2015,45(3):417-438(in Chinese with English abstract).
    [21] Jiang Y, Zhang HH, Li ZH, Deng YD, Song XY, Gu M, Sun JG. Design and optimization of multiclocked embedded systems using formal techniques. IEEE Trans. on Industrial Electronics, 2015,62(2):1270-1278.
    [22] Jiang Y, Zhang HH, Zhang HF, Liu H, Song XY, Gu M, Sun JG. Design of mixed synchronous/asynchronous systems with multiple clocks. IEEE Trans. on Parallel Distributed Systems, 2015,26(8):2220-2232.
    [23] Bae K, Olveczky PC, Feng TH, Tripakis S. Verifying ptolemy II discrete-event models using real-time maude. In:Proc. of the Int'l Conf. on Formal Engineering Methods. 2009. 717-736.
    附中文参考文献:
    [2] 王戟,詹乃军,冯新宇,刘志明.形式化方法概貌.软件学报,2019,30(1):33-61. http://www.jos.org.cn/1000-9825/5652.htm[doi:10.13328/j.cnki.jos.005652]
    [3] 林惠民,张文辉.模型检测:理论、方法与应用.电子学报,2002,30(z1):1907-1912.
    [13] 柳毅,麻志毅,何啸,邵维忠.一种从UML模型到可靠性分析模型的转换方法.软件学报,2010,21(2):287-304. http://www.jos.org.cn/1000-9825/3792.htm[doi:10.3724/SP.J.1001.2010.03792]
    [14] 杨志斌,胡凯,赵永望,马殿富,Bodeveix JP.基于时间抽象状态机的AADL模型验证.软件学报,2015,26(2):202-222. http://www.jos.org.cn/1000-9825/4776.htm[doi:10.13328/j.cnki.jos.004776]
    [20] 郭丹青,吕继东,王淑灵,唐涛,詹乃军,周达天.中国高速铁路列控系统的形式化分析与验证.中国科学:信息科学,2015,45(3):417-438.
    Related
    Cited by
    Comments
    Comments
    分享到微博
    Submit
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:1936
  • PDF: 5095
  • HTML: 3475
  • Cited by: 0
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 first2032497Visitors
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