Leverageable Semantics Definitions and Contract Reasoning for a Technical Architecture Description Language

ABSTRACT

The Architecture and Analysis Definition Language (AADL) is an industry standard modeling language distinguished by its emphasis on strong semantics for modeling real-time embedded systems. These features have led to AADL being used in several US Department of Defense formal-methods-oriented research projects addressing critical systems (e.g., DARPA’s HACMS and CASE programs) and is part of the US Army’s Architecture Centric Virtual Integration Process (ACVIP) which is applied on the Future Vertical Lift (FVL) Mission Systems Architecture Demonstration (MSAD) and Future Attack Reconnaissance Aircraft (FARA) acquisition. As an example of its strong semantics for modeling elements, the AADL standard describes Run-Time Services (RTS) that code generation frameworks can implement to realize standardized thread dispatch and port-based communications. However, the documentation of these semantics in the current AADL standard is semi-formal, allowing for divergent interpretations, thus limiting interoperability when implementing analysis or code generation capabilities.

In this talk, we illustrate a rule-based operational semantics formalization of key aspects of the AADL RTS. We also describe additional services and support functions that altogether allow for realistic, interoperable, and assured implementations. This contribution provides a basis for: (a) a more rigorous semantic presentation in upcoming versions of the standard, (b) a common approach to assess compliance of AADL code generation and analysis tools, (c) a foundation for further formalization and mechanization of AADL semantics, and (d) a more unambiguous and interoperable representation of executable system architecture models.

This RTS formalization guides the design of HAMR (High-Assurance Modeling and Rapid Engineering) -- a multiple-platform code-generation, development, and verification toolchain for AADL-specified systems. HAMR's architecture factors code-generation through the RTS formalization, and HAMR uses the RTS as an abstract, platform-independent realization of execution semantics. This abstraction can be instantiated by backend translations for different platforms. Current supported translation targets are: (1) Slang (a safety-critical subset of Scala with JVM-based deployment as well as C code generation designed for embedded systems), (2) a C back-end for Linux with communication based on System V inter-process communication primitives, and (3) a C back-end for the seL4 verified micro-kernel being used in a number of US Department of Defense research projects.

This talk addresses the HCSS 2023 theme of “Semantically Rigorous and Integrated High-Level Abstractions”. We will describe how our work on the AADL RTS provides leverage-able formal semantics for a technical architecture modeling language (AADL) that enables developer-friendly formal methods that are integrated across models and code via the HAMR tool chain. In addition to describing the semantics framework above, we will give a brief overview of the following HAMR capabilities:

• The GUMBO AADL contract language enables key component-level properties to be specified in system-level models. Those contracts are automatically translated down into Slang code by HAMR. Slang component implementations are then automatically checked for conformance to the modelderived contracts using the Logika verification framework
• Systems generated by HAMR give rise to execution traces which can be checked for conformance against executable representations (and other forms of mechanization) of the operational semantics rules. This leverages an executable reference model written in a purely functional subset of Slang and derived from the operational semantics rules. HAMR is available under an open-source license, and the project website includes an example repository and collection of videos, tutorials, and classroom lecture materials (also suited for workforce training).

Author

Dr. John Hatcliff is a University Distinguished Professor and Lucas-Rathbone Professor of Engineering at Kansas State University working in the areas of safety-critical systems, software architectures, and software verification and certification. He leads the Laboratory on Specification, Analysis, and Transformation of Software (SAnToS Lab), whose research has been funded by national funding agencies and companies including Department of Defense, National Science Foundation, DARPA, Department of Homeland Security, US Army, NASA, NIH, ARO, Air Force Office of Scientific Research, SEI, Collins Aerospace, Adventium Labs, Galois, and Lockheed Martin.