System-Level Design, Modeling, and Verification of GALS Cyber-Physical Systems
Cyber-physical systems (CPSs) are of great significance to industrial automation due to their proficiency in managing complex tasks. Concurrency and heterogeneity, which are fundamental characteristics of CPS, pose significant challenges related to complexities in design, system architecture, timing...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IEEE
2025-01-01
|
| Series: | IEEE Open Journal of the Industrial Electronics Society |
| Subjects: | |
| Online Access: | https://ieeexplore.ieee.org/document/11087690/ |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1849243595861655552 |
|---|---|
| author | Weiyi Zhang Zoran Salcic Avinash Malik |
| author_facet | Weiyi Zhang Zoran Salcic Avinash Malik |
| author_sort | Weiyi Zhang |
| collection | DOAJ |
| description | Cyber-physical systems (CPSs) are of great significance to industrial automation due to their proficiency in managing complex tasks. Concurrency and heterogeneity, which are fundamental characteristics of CPS, pose significant challenges related to complexities in design, system architecture, timing behavior, semantics, and cyber-physical interdependencies. We propose a system-level approach that leverages the globally asynchronous locally synchronous (GALS) model of computation to offer a structured and correct-by-construction methodology. The research also features a unified colored Petri nets (CPNs)-based modeling framework that bridges cyber and physical domains and enables holistic system verification. The approach comprises three stages: 1) design using SystemGALS for cyber-domain control and data flow, alongside Simulink for physical process modeling; 2) integration of CPN derived from SystemGALS and Simulink for unified representation; 3) formal analysis on the CPN model. In this article, we elaborate on each step of the system-level approach and provide an industrial automation use case for illustration. |
| format | Article |
| id | doaj-art-57bcf546bc3c4cd2991c977bd092a60c |
| institution | Kabale University |
| issn | 2644-1284 |
| language | English |
| publishDate | 2025-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Open Journal of the Industrial Electronics Society |
| spelling | doaj-art-57bcf546bc3c4cd2991c977bd092a60c2025-08-20T03:59:25ZengIEEEIEEE Open Journal of the Industrial Electronics Society2644-12842025-01-0161137115110.1109/OJIES.2025.359138911087690System-Level Design, Modeling, and Verification of GALS Cyber-Physical SystemsWeiyi Zhang0https://orcid.org/0000-0003-4915-1080Zoran Salcic1https://orcid.org/0000-0001-7714-9848Avinash Malik2https://orcid.org/0000-0002-7524-8292Department of Electrical, Computer and Software Engineering, University of Auckland, Auckland, New ZealandDepartment of Electrical, Computer and Software Engineering, University of Auckland, Auckland, New ZealandDepartment of Electrical, Computer and Software Engineering, University of Auckland, Auckland, New ZealandCyber-physical systems (CPSs) are of great significance to industrial automation due to their proficiency in managing complex tasks. Concurrency and heterogeneity, which are fundamental characteristics of CPS, pose significant challenges related to complexities in design, system architecture, timing behavior, semantics, and cyber-physical interdependencies. We propose a system-level approach that leverages the globally asynchronous locally synchronous (GALS) model of computation to offer a structured and correct-by-construction methodology. The research also features a unified colored Petri nets (CPNs)-based modeling framework that bridges cyber and physical domains and enables holistic system verification. The approach comprises three stages: 1) design using SystemGALS for cyber-domain control and data flow, alongside Simulink for physical process modeling; 2) integration of CPN derived from SystemGALS and Simulink for unified representation; 3) formal analysis on the CPN model. In this article, we elaborate on each step of the system-level approach and provide an industrial automation use case for illustration.https://ieeexplore.ieee.org/document/11087690/Cyber-physical systems (CPSs)formal models and methodsglobally asynchronous locally synchronous (GALS)Petri nets (PNs) |
| spellingShingle | Weiyi Zhang Zoran Salcic Avinash Malik System-Level Design, Modeling, and Verification of GALS Cyber-Physical Systems IEEE Open Journal of the Industrial Electronics Society Cyber-physical systems (CPSs) formal models and methods globally asynchronous locally synchronous (GALS) Petri nets (PNs) |
| title | System-Level Design, Modeling, and Verification of GALS Cyber-Physical Systems |
| title_full | System-Level Design, Modeling, and Verification of GALS Cyber-Physical Systems |
| title_fullStr | System-Level Design, Modeling, and Verification of GALS Cyber-Physical Systems |
| title_full_unstemmed | System-Level Design, Modeling, and Verification of GALS Cyber-Physical Systems |
| title_short | System-Level Design, Modeling, and Verification of GALS Cyber-Physical Systems |
| title_sort | system level design modeling and verification of gals cyber physical systems |
| topic | Cyber-physical systems (CPSs) formal models and methods globally asynchronous locally synchronous (GALS) Petri nets (PNs) |
| url | https://ieeexplore.ieee.org/document/11087690/ |
| work_keys_str_mv | AT weiyizhang systemleveldesignmodelingandverificationofgalscyberphysicalsystems AT zoransalcic systemleveldesignmodelingandverificationofgalscyberphysicalsystems AT avinashmalik systemleveldesignmodelingandverificationofgalscyberphysicalsystems |