微信服务号

微信订阅号

2025年3月24日 10:37 星期一
首页 > 过刊浏览>2021年第32卷第6期 >1830-1848. DOI:10.13328/j.cnki.jos.006252
PDF HTML阅读 XML下载 导出引用 引用提醒
Ptolemy离散事件模型形式化验证方法
作者:
作者简介:

陆芝浩(1995-),男,硕士,CCF学生会员,主要研究领域为形式化验证.
关永(1966-),男,博士,教授,博士生导师,CCF专业会员,主要研究领域为形式化验证,高可靠嵌入式系统.
王瑞(1981-),女,博士,教授,博士生导师,CCF专业会员,主要研究领域为形式化方法,软件安全验证.
施智平(1974-),男,博士,教授,博士生导师,CCF高级会员,主要研究领域为形式化方法,人工智能.
孔辉(1978-),男,博士,CCF专业会员,主要研究领域为形式化方法,混杂系统验证.

通讯作者:

王瑞，rwang04@cnu.edu.cn

基金项目:

国家自然科学基金（61877040，61876111）；首都师范大学交叉研究院项目（19530012005）


Formal Verification of Ptolemy Discrete Event Model
Author:
Fund Project:

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

  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [29]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

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

    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.

    参考文献
    [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.
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

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

复制
分享
文章指标
  • 点击次数:1926
  • 下载次数: 5081
  • HTML阅读次数: 3446
  • 引用次数: 0
历史
  • 收稿日期:2020-08-30
  • 最后修改日期:2020-10-26
  • 在线发布日期: 2021-02-07
  • 出版日期: 2021-06-06
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号