Paper Info
Title
Petri Net Based Specification and Verification of Globally-Asynchronous-Locally-Synchronous System
Abstract
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.
Year
DOI
Venue
2011
10.1007/978-3-642-19170-1_26
IFIP Advances in Information and Communication Technology
Keywords
Field
DocType
GALS,Embedded Systems,Petri Nets,Maude,Verification
Petri net,Globally asynchronous locally synchronous,Computer science,Communication channel,Input/output,State space,Semantics,Distributed computing
Conference
Volume
ISSN
Citations 
349
1868-4238
1
PageRank 
References 
Authors
0.43
3
8
Name
Order
Citations
PageRank
Filipe Moutinho1507.28
Luis Gomes225331.39
Paulo E. S. Barbosa3235.14
João Paulo Barros410518.03
Franklin Ramalho56512.86
Jorge Figueiredo6363.68
Aniko Costa75213.92
André Monteiro842.19