Please use this identifier to cite or link to this item: http://hdl.handle.net/1822/905

TitleModel checking embedded systems with PROMELA
Author(s)Ribeiro, Óscar R.
Fernandes, João M.
Pinto, Luís F.
Issue dateApr-2005
PublisherIEEE
Abstract(s)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.
TypeConference paper
DescriptionComunicação apresentada ao IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS 2005), 12, Washington, 2005.
URIhttp://hdl.handle.net/1822/905
ISBN0769523080
Peer-Reviewedyes
AccessOpen access
Appears in Collections:CAlg - Artigos em livros de atas/Papers in proceedings
CMAT - Artigos em atas de conferências e capítulos de livros com arbitragem / Papers in proceedings of conferences and book chapters with peer review
DMA - Comunicações

Files in This Item:
File Description SizeFormat 
2005-ECBS-Ribeiro.pdf269,59 kBAdobe PDFView/Open

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu ORCID