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 条

[21] Model Checking Self-Stabilising in Embedded Systems with Linear Temporal Logic [J].

Marah, Rim ;

EL Hibaoui, Abdelaaziz .

INTERNATIONAL JOURNAL OF ADVANCED COMPUTER SCIENCE AND APPLICATIONS, 2015, 6 (08) :256-261

[22] Design process of embedded automotive systems - Using model checking for correct specifications [J].

Jansen, P .

CORRECT HARDWARE DESIGN AND VERIFICATION METHODS, 1999, 1703 :2-7

[23] DEv-PROMELA: modeling, verification, and validation of a video game by combining model-checking and simulation [J].

Yacoub, Aznam ;

Hamri, Maamar El Amine ;

Frydman, Claudia .

SIMULATION-TRANSACTIONS OF THE SOCIETY FOR MODELING AND SIMULATION INTERNATIONAL, 2020, 96 (11) :881-910

[24] LIMITING STATE SPACE EXPLOSION OF MODEL CHECKING USING DISCRETE EVENT SIMULATION: COMBINING DEVS AND PROMELA [J].

Khemiri, Abdelhak ;

Hamri, Maamar El Amine ;

Frydman, Claudia ;

Pinaton, Jacques .

PROCEEDINGS OF THE 2019 SUMMER SIMULATION CONFERENCE (SUMMERSIM '19), 2019,

[25] Modeling and testing embedded system by model checking [J].

Sun, Fuzhen ;

Song, Dandan ;

Liao, Lejian ;

Li, Guoqiang .

International Journal of Advancements in Computing Technology, 2012, 4 (17) :18-27

[26] Model Checking of Embedded Systems Using RTCTL while Generating Timed Kripke Structure [J].

Wu, Yajun ;

Yamane, Satoshi .

2018 IEEE 42ND ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), VOL 1, 2018, :257-257

[27] Regression Testing Prioritization Based on Model Checking for Safety-Crucial Embedded Systems [J].

Sun, Fuzhen ;

Li, Yan .

2013 FOURTH INTERNATIONAL CONFERENCE ON DIGITAL MANUFACTURING AND AUTOMATION (ICDMA), 2013, :979-983

[28] Model checking embedded adaptive cruise controllers [J].

Nenchev, Vladislav .

ROBOTICS AND AUTONOMOUS SYSTEMS, 2023, 167

[29] Incremental bounded model checking for embedded software [J].

Schrammel, Peter ;

Kroening, Daniel ;

Brain, Martin ;

Martins, Ruben ;

Teige, Tino ;

Bienmueller, Tom .

FORMAL ASPECTS OF COMPUTING, 2017, 29 (05) :911-931

[30] Verifying Protocol Conformance Using Software Model Checking for the Model-Driven Development of Embedded Systems [J].

Moffett, Yann ;

Dingel, Juergen ;

Beaulieu, Alain .

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2013, 39 (09) :1307-1325

← 1 2 3 4 5 →