Formal Model Engineering of Distributed CPSs Using AADL: From Behavioral AADL Models to Multirate Hybrid Synchronous AADL
- Title
- Formal Model Engineering of Distributed CPSs Using AADL: From Behavioral AADL Models to Multirate Hybrid Synchronous AADL
- Authors
- Bae, Kyungmin; Ölveczky, Peter Csaba
- Date Issued
- 2023-10-19
- Publisher
- Open University of the Netherlands
- Abstract
- A promising way of integrating formal methods into industrial system design is to endow industrial modeling tools with automatic formal analyses. In this paper we identify some challenges for providing such formal methods “backends” for cyber-physical systems (CPSs), and argue that Maude could meet these challenges. We then give an overview of our research on integrating Maude analysis into the OSATE tool environment for the industrial CPS modeling standard AADL.
Since many critical distributed CPSs are “logically synchronous,” a key feature making automatic formal analysis practical is the use of synchronizers for CPSs. We identify a sublanguage of AADL to describe synchronous CPS designs. We can then use Maude to effectively verify such synchronous designs, which under certain conditions also verifies the corresponding asynchronous distributed systems, with clock skews and communication delays. We then explain how we have extended our methods to multirate systems and to CPSs with continuous behaviors.
We illustrate the effectiveness of Maude-based formal model engineering of industrial CPSs on avionics control systems and collections of drones. Finally, we identify future directions in this line of research.
- URI
- https://oasis.postech.ac.kr/handle/2014.oak/121475
- Article Type
- Conference
- Citation
- 19th International Conference on Formal Aspects of Component Software (FACS 2023), page. 127 - 152, 2023-10-19
- Files in This Item:
- There are no files associated with this item.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.