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

Filipe Moutinho; Luís Filipe dos Santos Gomes; Anikó Katalin Horváth da Costa

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

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

Filipe Moutinho, Luís Filipe dos Santos Gomes, Anikó Katalin Horváth da Costa

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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 language	Unknown
Title of host publication	IFIP Advances in Information and Communication Technology
Pages	237-245
Volume	349
DOIs	https://doi.org/10.1007/978-3-642-19170-1_26
Publication status	Published - 1 Jan 2011
Event	2nd IFIP WG 5.5/SOCOLNET Doctoral Conference on Computing, Electrical and Industrial Systems - Costa da Caparica, Portugal Duration: 21 Feb 2011 → 23 Feb 2011

Conference

Conference	2nd IFIP WG 5.5/SOCOLNET Doctoral Conference on Computing, Electrical and Industrial Systems
Country/Territory	Portugal
City	Costa da Caparica
Period	21/02/11 → 23/02/11

Access to Document

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

http://oa.uninova.pt/4972/

Cite this

@inproceedings{a3bbad1a45404f9484c1fefeaa15bfda,

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",

keywords = "GALS, Maude, Verification, Petri Nets, Embedded Systems",

author = "Filipe Moutinho and Gomes, {Lu{\'i}s Filipe dos Santos} and Costa, {Anik{\'o} Katalin Horv{\'a}th da}",

year = "2011",

month = jan,

day = "1",

doi = "10.1007/978-3-642-19170-1_26",

language = "Unknown",

isbn = "978-3-642-19170-1",

volume = "349",

pages = "237--245",

booktitle = "IFIP Advances in Information and Communication Technology",

note = "2nd IFIP WG 5.5/SOCOLNET Doctoral Conference on Computing, Electrical and Industrial Systems ; Conference date: 21-02-2011 Through 23-02-2011",

}

Moutinho, F , Gomes, LFDS & Costa, AKHD 2011, Petri Net Based Specification and Verification of Globally-Asynchronous-Locally-Synchronous System. in IFIP Advances in Information and Communication Technology. vol. 349, pp. 237-245, 2nd IFIP WG 5.5/SOCOLNET Doctoral Conference on Computing, Electrical and Industrial Systems, Costa da Caparica, Portugal, 21/02/11. https://doi.org/10.1007/978-3-642-19170-1_26

Petri Net Based Specification and Verification of Globally-Asynchronous-Locally-Synchronous System. / Moutinho, Filipe ; Gomes, Luís Filipe dos Santos ; Costa, Anikó Katalin Horváth da.
IFIP Advances in Information and Communication Technology. Vol. 349 2011. p. 237-245.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

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

AU - Moutinho, Filipe

AU - Gomes, Luís Filipe dos Santos

AU - Costa, Anikó Katalin Horváth da

PY - 2011/1/1

Y1 - 2011/1/1

N2 - 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

AB - 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

KW - GALS

KW - Maude

KW - Verification

KW - Petri Nets

KW - Embedded Systems

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

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

M3 - Conference contribution

SN - 978-3-642-19170-1

VL - 349

SP - 237

EP - 245

BT - IFIP Advances in Information and Communication Technology

T2 - 2nd IFIP WG 5.5/SOCOLNET Doctoral Conference on Computing, Electrical and Industrial Systems

Y2 - 21 February 2011 through 23 February 2011

ER -