loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
12th IEEE International Conference and Workshops on the Engineering of Computer-Based Systems (ECBS'05)
Model Checking Embedded Systems with PROMELA
Greenbelt, Maryland
April 04-April 07
ISBN: 0-7695-2308-0
ASCII Text
x 
 
Óscar R. Ribeiro, João M. Fernandes, Luís F. Pinto, "Model Checking Embedded Systems with PROMELA," Engineering of Computer-Based Systems, IEEE International Conference on the, pp. 378-385, 12th IEEE International Conference and Workshops on the Engineering of Computer-Based Systems (ECBS'05), 2005.
 
 
BibTex
x
 
@article{ 10.1109/ECBS.2005.53,
author = {Óscar R. Ribeiro and João M. Fernandes and Luís F. Pinto},
title = {Model Checking Embedded Systems with PROMELA},
journal ={Engineering of Computer-Based Systems, IEEE International Conference on the},
volume = {0},
year = {2005},
isbn = {0-7695-2308-0},
pages = {378-385},
doi = {http://doi.ieeecomputersociety.org/10.1109/ECBS.2005.53},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Engineering of Computer-Based Systems, IEEE International Conference on the
TI - Model Checking Embedded Systems with PROMELA
SN - 0-7695-2308-0
SP378
EP385
A1 - Óscar R. Ribeiro,
A1 - João M. Fernandes,
A1 - Luís F. Pinto,
PY - 2005
KW - null
VL - 0
JA - Engineering of Computer-Based Systems, IEEE International Conference on the
ER -
 
Óscar R. Ribeiro, Universidade do Minho
João M. Fernandes, Universidade do Minho
Luís F. Pinto, Universidade do Minho
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.
Citation:
Óscar R. Ribeiro, João M. Fernandes, Luís F. Pinto, "Model Checking Embedded Systems with PROMELA," ecbs, pp.378-385, 12th IEEE International Conference and Workshops on the Engineering of Computer-Based Systems (ECBS'05), 2005
Usage of this product signifies your acceptance of the Terms of Use.