Autor(es):
Ribeiro, Óscar R. 
; Fernandes, João M.
Data: 2007
Identificador Persistente: http://hdl.handle.net/1822/11008
Origem: RepositóriUM - Universidade do Minho
Detalhes do Documento
Translating synchronous Petri Nets into PROMELA for verifying behavioural prope...
Descrição
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.
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 de Documento
Documento de conferência
Idioma Inglês
Idioma Inglês
| Financiadores do RCAAP | |||||||
|
|
|
|
|
|
||