Author(s): Moutinho, Filipe ; Gomes, Luís ; Barbosa, Paulo ; Barros, João Paulo ; Ramalho, Franklin ; Figueiredo, Jorge ; Costa, Aniko ; Monteiro, Andre ; Barros, João Paulo
Date: 2011
Persistent ID: http://hdl.handle.net/20.500.12207/654
Origin: Repositório Institucional do IPBeja
Subject(s): GALS; Embedded systems; Petri Nets; Maude; Synchronous system
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.
