Model checking embedded systems with PROMELA

被引：5
|
作者：
Ribeiro, OR [1 ]
Fernandes, JM [1 ]
Pinto, LF [1 ]
机构：
[1] Univ Minho, Dept Informat, Braga, Portugal
来源：
12TH IEEE INTERNATIONAL CONFERENCE AND WORKSHOPS ON THE ENGINEERING OF COMPUTER-BASED SYSTEMS, PROCEEDINGS | 2005年
关键词：
D O I：
10.1109/ECBS.2005.53
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
The design process for embedded systems can benefit from the usage of formal methods. if some properties of the systems are checked, before design and implementation decisions are accomplished. This paper presents a model checking approach using the Spin tool, to verify some important properties of embedded systems, namely liveness, deadlock-freedom, and structural conflicts among transitions. The systems are modelled with a variant of Petri Nets, called SIPN (Synchronous and Interpreted Petri Nets), and this paper discusses how SIPN models should be specified with the PROMELA language (input format for the Spin model checker). The approach is exemplified with a case study.
引用
收藏
页码：378 / 385
页数：8
相关论文
共 50 条
  • [41] Model Checking of Embedded Assembly Program Based on Simulation
    Yamane, Satoshi
    Konoshita, Ryosuke
    Kato, Tomonori
    IEICE TRANSACTIONS ON INFORMATION AND SYSTEMS, 2017, E100D (08): : 1819 - 1826
  • [42] A model checking tool embedded into services composition environment
    Gao, Chunming
    Liu, Rongsheng
    Song, Yan
    Chen, Huowang
    GCC 2005: FIFTH INTERNATIONAL CONFERENCE ON GRID AND COOPERATIVE COMPUTING, PROCEEDINGS, 2006, : 355 - +
  • [43] Efficient modeling of embedded memories in bounded model checking
    Ganai, MK
    Gupta, A
    Ashar, P
    COMPUTER AIDED VERIFICATION, 2004, 3114 : 440 - 452
  • [44] Model Checking Applied to Embedded Software of University Satellite
    Alencar, Waldo A. F.
    Villani, Emilia
    JOURNAL OF CONTROL AUTOMATION AND ELECTRICAL SYSTEMS, 2014, 25 (01) : 126 - 136
  • [45] Case studies of model checking for embedded system designs
    Chen, X
    Hsieh, H
    Balarin, F
    Watanabe, Y
    THIRD INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN, PROCEEDINGS, 2003, : 20 - 28
  • [46] Modeling Railway Control Systems in Promela
    Nardone, Roberto
    Gentile, Ugo
    Benerecetti, Massimo
    Peron, Adriano
    Vittorini, Valeria
    Marrone, Stefano
    Mazzocca, Nicola
    FORMAL TECHNIQUES FOR SAFETY-CRITICAL SYSTEMS, (FTSCS 2015), 2016, 596 : 121 - 136
  • [47] Challenges in Embedded Model Checking - A Simulator for the [mc]square Model Checker
    Reinbacher, Thomas
    Kramer, Michael
    Horauer, Martin
    Schlich, Bastian
    2008 INTERNATIONAL SYMPOSIUM ON INDUSTRIAL EMBEDDED SYSTEMS, 2008, : 245 - +
  • [48] Local-Memory-Based Integrity Checking for Embedded Systems
    Li, Ning
    Nakajima, Tatsuo
    2013 IEEE 16TH INTERNATIONAL CONFERENCE ON COMPUTATIONAL SCIENCE AND ENGINEERING (CSE 2013), 2013, : 742 - 750
  • [49] Checking the Conformance of a Promela Design to its Formal Specification in Event-B
    Vu, Dieu-Huong
    Chiba, Yuki
    Yatake, Kenro
    Aoki, Toshiaki
    FORMAL TECHNIQUES FOR SAFETY-CRITICAL SYSTEMS, FTSCS 2014, 2015, 476 : 110 - 126
  • [50] Verifying distributed real-time properties of embedded systems via graph transformations and model checking
    Gabor Madl
    Sherif Abdelwahed
    Douglas C. Schmidt
    Real-Time Systems, 2006, 33 : 77 - 100
12345