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 条
  • [1] Model checking learning agent systems using Promela with embedded C code and abstraction
    Kirwan, Ryan
    Miller, Alice
    Porr, Bernd
    FORMAL ASPECTS OF COMPUTING, 2016, 28 (06) : 1027 - 1056
  • [2] A generalized semantics of PROMELA for abstract model checking
    Gallardo, MD
    Merino, P
    Pimentel, E
    FORMAL ASPECTS OF COMPUTING, 2004, 16 (03) : 166 - 193
  • [3] Abstraction Framework and Complexity of Model Checking Based on the Promela Models
    Chen Daoxi
    Zhang Guangquan
    Fan Jianxi
    ICCSSE 2009: PROCEEDINGS OF 2009 4TH INTERNATIONAL CONFERENCE ON COMPUTER SCIENCE & EDUCATION, 2009, : 857 - 861
  • [4] Motivating Model Checking of Embedded Systems Software
    Reinbacher, Thomas
    Kramer, Michael
    Horauer, Martin
    Schlich, Bastian
    PROCEEDINGS OF 2008 IEEE/ASME INTERNATIONAL CONFERENCE ON MECHATRONIC AND EMBEDDED SYSTEMS AND APPLICATIONS, 2008, : 546 - +
  • [5] Model checking embedded and real time systems
    Larsen, Kim G.
    WODES' 08: PROCEEDINGS OF THE 9TH INTERNATIONAL WORKSHOP ON DISCRETE EVENT SYSTEMS, 2008, : 260 - 260
  • [6] Synthesizing Promela model sketches using abstract lifted model checking
    Dimovski A.S.
    International Journal of Information Technology, 2024, 16 (1) : 425 - 435
  • [7] A Spin / Promela Application for Model checking UML Sequence Diagrams
    Vidal-Silva, Cristian L.
    Villarroel, Rodolfo
    Rubio, Jose
    Johnson, Franklin
    Madariaga, Erika
    Campos, Camilo
    Carter, Luis
    INTERNATIONAL JOURNAL OF ADVANCED COMPUTER SCIENCE AND APPLICATIONS, 2018, 9 (10) : 586 - 599
  • [8] Formal coverification of embedded systems using model checking
    Cortés, LA
    Eles, P
    Peng, Z
    PROCEEDINGS OF THE 26TH EUROMICRO CONFERENCE, VOLS I AND II, 2000, : 106 - 113
  • [9] Model checking C source code for embedded systems
    Bastian Schlich
    Stefan Kowalewski
    International Journal on Software Tools for Technology Transfer, 2009, 11 (3) : 187 - 202
  • [10] Model checking the observational determinism security property using PROMELA and SPIN
    Dabaghchian, Maryam
    Azgomi, Mohammad Abdollahi
    FORMAL ASPECTS OF COMPUTING, 2015, 27 (5-6) : 789 - 804
12345