HAMR - High-Assurance Modeling and Rapid Engineering for Embedded Systems Using AADL

Presented as part of the 2021 HCSS conference. 

ABSTRACT

Many domains rely on real-time embedded systems that require high levels of assurance. Assurance of such systems is challenging due to the need to support compositionality related to platform-based development, software product lines, interoperability, and system-of-system concepts. The Architecture and Analysis Definition Language (AADL) provides a modeling framework that emphasizes componentbased development, modeling elements with semantics capturing common embedded system threading and communication patterns, and standardized run-time service interfaces. Through its annex languages and tool plug-in extensibility mechanisms, it also supports a variety of architecture specification and analyses including component behavioral contracts, hazard analysis, schedulability analysis, dependence analysis, etc. The AADL vision emphasizes being able to prototype, assure, and deploy system implementations derived from the models. This talk will present an overview of HAMR (High-Assurance Modeling and Rapid Engineering) -- a multipleplatform code-generation, development, and verification tool-chain for AADL-specified systems. HAMR's architecture factors code-generation through AADL's standardized run-time services (RTS). HAMR uses the AADL RTS as an abstract platform-independent realization of execution semantics which 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. The C generated by HAMR is also compatible with the CompCert verified C compiler. HAMR supports integrations with other languages (e.g., CakeML) through its generated AADL RTS foreign-function interface facilities.

The talk will describe experience with HAMR on the DARPA CASE (Cyber-Assured System Engineering) project. On CASE, AADL is used to model defense systems and to enable component-based model-based transformations that enhance system architecture to achieve greater cyber-resiliency. HAMR is then used to support development and deployment on the seL4 microkernel. SeL4’s formally-verified partitioning and memory security properties provide the foundation for cyber-resiliency assurance arguments. The talk addresses the HCSS 2021 theme of “Exploring Compositionality”. The HAMR work explores how domain-specific threading and communication abstractions (“reasoning in domain-specific settings” from the HCSS announcement) can be used as compositional building blocks for embedded systems (“horizontal”, i.e., component-to-component composition) and how formally verified partitioning platforms such as seL4 can support compositional system assurance. HAMR also utilizes AADL’s standardized RTS to form an abstract semantic reference model of computation -- enabling components to be “vertically” composed onto different platforms as the RTS abstraction layer is instantiated to conforming backend platforms. HAMR is available under an open-source license, and the project web-site includes an example repository and collection of videos, tutorials, and classroom lecture materials (also suited for workforce training).

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, and Lockheed Martin.

Dr. Hatcliff recently led the primary technical working group for the AAMI / UL 2800 Joint Committee that is developing safety and security standards for medical device interoperability. The focus of Dr. Hatcliff’s current funded research includes developing model-based verification and hazard analysis techniques for safety/security-critical embedded systems, and automated software contract verification for modern languages for embedded systems.