Formal Model Engineering of Distributed CPSs Using AADL: From Behavioral AADL Models to Multirate Hybrid Synchronous AADL

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.