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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Citations (Scopus)

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
Original languageUnknown
Title of host publicationIFIP Advances in Information and Communication Technology
Pages237-245
Volume349
DOIs
Publication statusPublished - 1 Jan 2011
Event2nd IFIP WG 5.5/SOCOLNET Doctoral Conference on Computing, Electrical and Industrial Systems -
Duration: 1 Jan 2011 → …

Conference

Conference2nd IFIP WG 5.5/SOCOLNET Doctoral Conference on Computing, Electrical and Industrial Systems
Period1/01/11 → …

Cite this