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

被引:0
|
作者
Moutinho, Filipe [1 ,2 ]
Gomes, Luis [1 ,2 ]
Barbosa, Paulo [3 ]
Barros, Joao Paulo [2 ,4 ]
Ramalho, Franklin [3 ]
Figueiredo, Jorge [3 ]
Costa, Aniko [1 ,2 ]
Monteiro, Andre [3 ]
机构
[1] Univ Nova Lisboa, Fac Ciencias & Tecnol, P-1200 Lisbon, Portugal
[2] Univ Nova Lisboa, Caparica, Portugal
[3] Univ Fed Campina Grande, Campina Grande, Brazil
[4] Escola Super Tecnol & Gestao, Inst Politecn Beja, Beja, Portugal
关键词
GALS; Embedded Systems; Petri Nets; Maude; Verification;
D O I
暂无
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
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.
引用
收藏
页码:237 / +
页数:2
相关论文
共 50 条
  • [1] Designing Globally-Asynchronous-Locally-Synchronous System from Multi-Rate Simulink Model
    Shi, Yiqiong
    Gwee, Bah-Hwee
    [J]. 2013 IEEE 11TH INTERNATIONAL NEW CIRCUITS AND SYSTEMS CONFERENCE (NEWCAS), 2013,
  • [2] Synchronous-Logic and Globally-Asynchronous-Locally-Synchronous (GALS) Acoustic Digital Signal Processors
    Chong, Kwen-Siong
    Chang, Kok-Leong
    Gwee, Bah-Hwee
    Chang, Joseph S.
    [J]. IEEE JOURNAL OF SOLID-STATE CIRCUITS, 2012, 47 (03) : 769 - 780
  • [3] GRL: A Specification Language for Globally Asynchronous Locally Synchronous Systems
    Jebali, Fatma
    Lang, Frederic
    Mateescu, Radu
    [J]. FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2014, 2014, 8829 : 219 - 234
  • [4] Modeling and verification of globally asynchronous and locally synchronous ring architectures
    Dasgupta, S
    Yakovlev, A
    [J]. DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION, VOLS 1 AND 2, PROCEEDINGS, 2005, : 568 - 569
  • [5] FLEXIBLE MULTICORE SYSTEM BASED ON GLOBALLY ASYNCHRONOUS LOCALLY SYNCHRONOUS CORE
    Jain, Rashmi A.
    Padole, Dinesh V.
    [J]. 2015 FIFTH INTERNATIONAL CONFERENCE ON COMMUNICATION SYSTEMS AND NETWORK TECHNOLOGIES (CSNT2015), 2015, : 820 - 825
  • [6] Design Of A Globally Asynchronous Locally Synchronous Digital System
    Nagy, Lukas
    Koscelansky, Jan
    Stopjakova, Viera
    [J]. 12TH IEEE INTERNATIONAL CONFERENCE ON EMERGING ELEARNING TECHNOLOGIES AND APPLICATIONS (ICETA 2014), 2014, : 529 - 533
  • [8] Globally Asynchronous Locally Synchronous Design Based Heterogeneous Multi-core System
    Jain, Rashmi A.
    Padole, Dinesh V.
    [J]. ICT AND CRITICAL INFRASTRUCTURE: PROCEEDINGS OF THE 48TH ANNUAL CONVENTION OF COMPUTER SOCIETY OF INDIA - VOL I, 2014, 248 : 739 - 748
  • [9] Globally asynchronous locally synchronous FPGA architectures
    Royal, A
    Cheung, PYK
    [J]. FIELD-PROGRAMMABLE LOGIC AND APPLICATIONS, PROCEEDINGS, 2003, 2778 : 355 - 364
  • [10] Implementation of a Fault-Tolerant, Globally-Asynchronous-Locally-Synchronous, Inter-Chip NoC Communication Bridge on FPGAs
    Kyriakakis, Eleftherios
    Ngo, Kalle
    Oberg, Johnny
    [J]. 2017 IEEE NORDIC CIRCUITS AND SYSTEMS CONFERENCE (NORCAS): NORCHIP AND INTERNATIONAL SYMPOSIUM OF SYSTEM-ON-CHIP (SOC), 2017,