Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [8 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Friday, July 21, 2017 - 11:25:13 AM
Last modification on : Wednesday, June 1, 2022 - 1:56:02 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Filipe Moutinho, Luís Gomes, Paulo Barbosa, João Paulo Barros, Franklin Ramalho, et al.. Petri Net Based Specification and Verification of Globally-Asynchronous-Locally-Synchronous System. 2nd Doctoral Conference on Computing, Electrical and Industrial Systems (DoCEIS), Feb 2011, Costa de Caparica, Portugal. pp.237-245, ⟨10.1007/978-3-642-19170-1_26⟩. ⟨hal-01566548⟩



Record views


Files downloads