Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/11008
Título: | Translating synchronous Petri Nets into PROMELA for verifying behavioural properties |
Autor(es): | Ribeiro, Óscar R. Fernandes, João M. |
Data: | Jul-2007 |
Editora: | IEEE |
Citação: | INTERNATIONAL SYMPOSIUM ON INDUSTRIAL EMBEDDED SYSTEMS (SIES’2007), 2, Lisboa, Portugal, 2007 – “2007 Symposium on Industrial Embedded Systems Proceedings.” [S.l.] : IEEE, 2007. ISBN 1-4244-0840-7. p. 266-273. |
Resumo(s): | For developing embedded systems, the design process may benefit in some contexts from the usage of formal methods, namely to find critical errors and flaws, before final design and implementation decisions are taken. The Synchronous and Interpreted Petri Net (SIP-net) modelling language is considered in this article to model embedded systems. This model of computation is based on safe Petri nets with guarded transitions and synchronous transitions firing, and also includes enabling and inhibitor arcs. The Spin tool, whose input language is PROMELA, is a verification system based on model checking techniques. This article presents a program to translate SIP-net models into PROMELA code and discusses in detail the adequacy of the created PROMELA specification for verification through model checking techniques. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/11008 |
ISBN: | 1-4244-0840-7 |
DOI: | 10.1109/SIES.2007.4297344 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: | DI/CCTC - Artigos (papers) |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
2007-SIES-IEEE.pdf | 174,15 kB | Adobe PDF | Ver/Abrir |