HAMR - An AADL Multi-platform Code Generation Toolset.

This paper describes the High-Assurance Model-based Rapid engineering for embedded systems (HAMR) tool-kit that generates high-assurance software from standards-based system architecture models for embedded cyber-physical systems. HAMR’s computational model is based on standardized run-time services and communication models that together provide an abstract platform-independent realization which can be instantiated by back-end translations for different platforms. HAMR currently targets multiple platforms, including rapid prototyping targets such as Java Virtual Machines, Linux, as well as the formally verified seL4 space partitioned micro-kernel. HAMR bridges the gap between architecture models and the system implementation by generating high assurance infrastructure components that satisfy the requirements specified in the model and preserving rigorous execution semantics. Based on the architecture model, including the components, their interfaces, run-time performance properties, and inter-component connections, the HAMR-generated code creates Application Programming Interfaces that provide developer-centric ease-of-use, as well as support automated verification. HAMR currently interprets architecture models captured in the Architecture Analysis and Design Language (AADL). AADL is a rigorous standardized modeling language that has proven useful in the development of high assurance embedded systems. We describe using HAMR for building applications from safety and security-critical domains such as medical devices and avionics mission-systems.