Oqarina – Mechanization of the AADL Architectural Description Language

ABSTRACT

The SAE AADL standard [1] provides the foundations for describing the architecture of safety-critical cyber-physical systems. AADL is a modeling language, equipped with a syntax definition and several legality and consistency rules that define the notions of model validity and its semantics. Several research activities illustrated how AADL can be used to model complex systems and to analyze them for key quality attributes such as performance, safety, or security. Yet, AADL semantics is encoded in plain English and a few automata that have been transcribed into the core of toolsets such as OSATE by the SEI [2] and used intensively to derive other analysis techniques such as Assume/Guarantee contracts (Resolute and AGREE by Collins [3]), model-checking, or code generation as demonstrated by the Ocarina or HAMR toolsets. AADL has been tested in several DARPA projects such as HACCMS, CASE, or by the European Space Agency with the TASTE toolchain [4]. Such diversity illustrates that the core principles of AADL can be used to implement toolchains for designing and implementing safety-critical systems. Yet, the lack of a cohesive formal description of AADL semantics makes it difficult to compare tool capabilities or even assess they properly cover AADL semantics. Let us note this is not specific to AADL and applies to Model-Based Systems Engineering as a whole, including OMG SysML or UML.

Starting in 2021, the SEI has been investigating the mechanization of a large fragment of AADL using the Coq theorem prover: Oqarina -- https://github.com/Oqarina/oqarina. Our objective is to offer a new way of interacting with AADL models from within a theorem prover. Oqarina provides the following capabilities

• A representation of AADL declarative and instance models as Coq data types, capturing component categories and property sets
• A library of accessors to manipulate models
• An implementation of AADL legality and consistency rules as decidable propositions
• A reimplementation of Collins’ Resolute to write user-defined verification methods as static predicates
• A definition of the semantics of AADL component categories using operational semantics and a translation towards the DEVS formalism for simulating models
• Import of AADL instance models serialized in JSON

Oqarina builds on the lessons learned from the Ocarina AADL toolchain in defining AADL modeling processing capabilities. Oqarina serves as a proof of concept of “Rigorous Model-Based Systems Engineering”. Beyond the use of formal methods to process models, we are advocating for the use of formal methods, including theorem provers, to define MBSE itself. Oqarina demonstrates that using a theorem prover can achieve multiple goals to support a rigorous approach to defining MBSE by

• Substituting documents-based definition of MBSE processes with actual formal definitions that can be reviewed and combined for completeness and type correctness
• Leveraging formal methods to assure the correctness of verification methods in a MBSE toolchain

In this talk, I will provide an overview of the mechanization of AADL, illustrate how theorem provers support mechanizing the semantics of modeling languages, and AADL models can be proved correct.

This talk is a contribution to the “Semantically Rigorous and Integrated High-Level Abstractions” track of HCSS’23. It shows how to mechanize the semantics of higher levels of abstraction and apply sound verification techniques.

References

[1] AS-2C Architecture Analysis and Design Language. “Architecture Analysis & Design Language (AADL).” SAE International. Accessed May 3, 2021. https://doi.org/10.4271/AS5506D.

[2] OSATE toolkit. https://www.osate.org

[3] Gacek, Andrew, John Backes, Darren Cofer, Konrad Slind, and Mike Whalen. “Resolute: An Assurance Case Language for Architecture Models.” Ada Lett. 34, no. 3 (October 2014): 19–28. https://doi.org/10.1145/2692956.2663177.

[4] Perrotin, Maxime, Eric Conquet, Julien Delange, André Schiele, and Thanassis Tsiodras. “TASTE: A Real-Time Software Engineering Tool- Chain Overview, Status, and Future,” 26–37. SDL 2011: Integrating System and Software Modeling, LNCS, Vol. 7083, 2011. https://doi.org/10.1007/978-3-642-25264-8_4.

Author

Jerome Hugues is a Senior Researcher at the Software Engineering Institute on the Assuring Cyber-Physical Systems team. He holds a Habilitation (2017) from INP Toulouse, a Ph.D. (2005) and an engineering degree (2002) both from Telecom ParisTech, and an MSc in Computer Science from UPMC (2002). His research interests focus on the design of software-based real-time and embedded systems and tools to support it. He is a member of the SAE AS-2C committee working on the AADL since 2005. Before joining the CMU/SEI, he was a professor at the Department of Engineering of Complex Systems of ISAE-Supaero in Toulouse France, in charge of teaching curriculum on systems engineering, safety-critical systems, and real-time systems. He contributes to the OSATE, Ocarina, and TASTE AADL toolchains.

View Slides (You must register and request HCSS Community Membership to download the slides.)