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.