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 条

[31] Formalizing Real-Time Embedded System into Promela
Sukvanich, Punwess
Thongtak, Arthit
Vatanawood, Wiwat
2015 4TH INTERNATIONAL CONFERENCE ON MECHANICS AND CONTROL ENGINEERING (ICMCE 2015), 2015, 35
[32] Checking the Paths to Identify Mutant Application on Embedded Systems
Sere, Ahmadou Al Khary
Iguchi-Cartigny, Julien
Lanet, Jean-Louis
FUTURE GENERATION INFORMATION TECHNOLOGY, 2010, 6485 : 459 - +
[33] Checking the temporal behaviour of distributed and parallel embedded systems
Halang, WA
Kececi, N
Tsai, G
DESIGN AND ANALYSIS OF DISTRIBUTED EMBEDDED SYSTEMS, 2002, 91 : 153 - 162
[34] Model Checking Hybrid Systems
Clarke, Edmund M.
Gao, Sicun
LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: SPECIALIZED TECHNIQUES AND APPLICATIONS, PT II, 2014, 8803 : 385 - 386
[35] Model checking multiagent systems
Benerecetti, M
Giunchiglia, F
Serafini, L
JOURNAL OF LOGIC AND COMPUTATION, 1998, 8 (03) : 401 - 423
[36] Verification of embedded real-time systems using symbolic model checking: A case study
Duan, Z. (zhhduan@mail.xidian.edu.cn), 1600, Science and Engineering Research Support Society, 20 Virginia Court, Sandy Bay, Tasmania, Australia (06):
[37] Model-checking Framework for Embedded Systems Controllers Development using IOPT Petri Nets
Pereira, Fernando
Moutinho, Filipe
Gomes, Luis
2012 IEEE INTERNATIONAL SYMPOSIUM ON INDUSTRIAL ELECTRONICS (ISIE), 2012, : 1399 - 1404
[38] Model-Checking for the Functional Safety of Control Component-based Heterogeneous Embedded Systems
Khalgui, Mohamed
Hanisch, Hans-Michael
Gharbi, Atef
2009 IEEE CONFERENCE ON EMERGING TECHNOLOGIES & FACTORY AUTOMATION (EFTA 2009), 2009,
[39] A model checking approach to evaluating system level dynamic power management policies for embedded systems
Shukla, SK
Gupta, RK
SIXTH IEEE INTERNATIONAL HIGH-LEVEL DESIGN VALIDATION AND TEST WORKSHOP, PROCEEDINGS, 2001, : 53 - 57
[40] Applying Multi-Core Model Checking to Hardware-Software Partitioning in Embedded Systems
Trindade, Alessandro
Ismail, Hussama
Cordeiro, Lucas
2015 BRAZILIAN SYMPOSIUM ON COMPUTING SYSTEMS ENGINEERING (SBESC), 2015, : 102 - 105

← 1 2 3 4 5 →