Voltar
Capítulo de livro Acesso aberto Produção Nacional Revisado por pares
BIBTEX RIS

Petri Net Based Specification and Verification of Globally-Asynchronous-Locally-Synchronous System

2011; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-642-19170-1_26

ISSN

1868-422X

Autores

Filipe Moutinho, Lúıs Gomes, Paulo Barbosa, João Paulo Barros, Franklin Ramalho, Jorge Figueiredo, Anikó Costa, André Monteiro,

Tópico(s)

Real-Time Systems Scheduling

Resumo

This paper shows a methodology for Globally-Asynchronous-Locally-Synchronous (GALS) systems specification and verification. The distributed system is specified by non-autonomous Petri net modules, obtained after the partition of a (global) Petri net model. These modules are represented using IOPT (Input-Output Place-Transition) Petri net models, communicating through dedicated communication channels forming the GALS system under analysis. This set of modules is then automatically translated into Maude code through a MDA approach. As the modules of GALS systems run concurrently, the Maude semantics for concurrent objects is used along with message representation. Finally, as a particular case, the system state space is generated from the Maude specification of the GALS system, allowing property verification.

Referência(s)