HAMR Tour

Overview

This chapter provides a high-level summary of developer activities when using HAMR. This includes:

• simple illustrations of AADL component and system modeling,

• examples of HAMR-related AADL model analysis,

• generating code with HAMR,

• programming component behaviors with HAMR,

• HAMR-based testing for components (unit testing) and systems (system tests), and

• running HAMR applications.

HAMR supports multiple programming languages for coding the functionality of components and systems whose infrastructured is auto-generated from HAMR. Workflows for both Slang and C programming languages are illustrated in this chapter. The first two items above (AADL modeling and AADL analysis) are independent of whether or not Slang or C is being used as the programming language. Accordingly, the content of the chapter is organized as follows:

• AADL modeling

• AADL analysis

• Slang workflows

• C workflows

Throughout the presentation, forward references are provided to subsequent chapters that provide more details.

AADL Modeling

The OSATE Eclipse AADL Environment

HAMR workflows begin with creating AADL models of components and systems in the OSATE AADL tool. OSATE is based on the widely-used open-source Eclipse IDE. HAMR is currently distributed in special “branded” distribution of OSATE called the Formal Methods Integrated Development Environment (FMIDE) developed on the DARPA CASE project.

• See the installation instructions for installing OSATE/FMIDE and HAMR plug-in.

• See AADL Computational Paradigm and HAMR Fundamental Concepts for a detailed presentation of AADL modeling and semantics concepts.

Each OSATE AADL model has both a graphical view and textual view, and OSATE keeps them synchronized. Although it is possble to create and edit models in the graphical view, HAMR documentation emphasizes creating/editing models in the textual view and then visualizing them in the graphical view.

OSATE AADL Graphical View

OSATE AADL Textual View

OSATE includes different analysis and code generation plug-ins whose functions can be accessed through the menu system or through icons in the tool bar. Some OSATE/FMIDE capabilities require additional libraries to be installed, they vary in their maturity, and they work on different model features/properties (some of which may not be included in your models) – so the take away is that you should not expect all other OSATE plug-ins to work on models in the HAMR documentation nor models that you build. However, all HAMR-related related features described in this documentation should work.

OSATE Menus and Toolbar

Component Modeling

AADL systems are built from different kinds of components.

With HAMR, the most important component kind is a thread component, which corresponds to a real-time task in real-time systems literature.

HAMR generates code skeletons for thread components, and a developer implements a system by (a) using a HAMR-supported programming language to program the behavior of thread components and (b) using other AADL modeling elements to group and “wire” components together.

HAMR also generates for communication infrastructure for the wiring between components, and platform infrastructure code corresponding to other kinds of AADL components such as process and system – which are used to aggregate thread components so that they can be associated with various system resources and configurations.

Each AADL software component, e.g., a thread, process, or system, has a specified interface captured as an AADL component type. AADL emphasizes port-based inter-component communication, and so an AADL component type (interface) is a collection of ports. There are several categories of AADL ports (event, data, and event data), and a port category (together with optional port properties) indicates a particular pattern of communication to be used for communication on that port.

• data ports – roughly correspond to shared memory between components that act either as writers or readers

• event ports – roughly corespond to buffered notifications from one component to another

• event data ports – roughly correspond to buffered messages with payloads sent from one component to another

AADL properties can be used to configure buffer sizes, timing properties, etc.

HAMR only supports uni-directional ports and connections (with port direction indicated by in and out), so as to enable (a) clean design of security and information flow controls and (b) model- and code-level information flow analysis.

AADL Textual Representation of Port-based Thread Component Type (Interface)

Later in the workflow, HAMR will generate code-level interfaces for modeled component types.

Defining Data Types for Intercomponent Communication (shared data, messages)

AADL provides facilities modeling data structures like structs (records), arrays, unions, and enums that flow between components. AADL libraries also provide common base types including fixed-width, signed and unsigned integers, floats, etc. commonly used in embedded system programming.

Once these types are defined, they are referenced in component interface specification to indicate the types of data flowing across ports.

AADL Data Modeling

Later in the workflow, HAMR will generate code-level data types for modeled component types.

System Modeling

Software Integration and Architecture

Once software threads are designed, they can be integrated, aggregated into AADL thread group components, placed in address spaces (represented by AADL processes) — all of these elements can be organized to into subsystems (represented by AADL system components) and systems.

AADL Software System Modeling (AADL graphical view)

A key aspect of these integration activities is using AADL connections to associate the output ports of one component with the input ports of another. AADL’s type checking checks that connected ports are type compatible. Other AADL tools such as AGREE and BLESS can be used to specify contracts (formal specification of data constraints and input output relations) and then check that connected ports/components have compatible contracts.

AADL Software System Modeling (AADL textual view)

Once the software architecture is specified, HAMR can generate code for it (illustrated in later in the workflow). HAMR generates execution contexts, thread skeletons, and APIs for port communication for thread components. The developer fills in the thread skeletons to complete the component implementation.

HAMR generates code for communication between thread components using the target platform’s communication mechanisms which can include both local communication as well as distributed communication (e.g., supported by middleware). Realization of inter-component communication is completely automatic. That is, in contrast to realizing threads, for communication infrastructure all the code is generated – there are no skeletons to fill in.

HAMR code generation may be repeated as models are updated. HAMR code generation organizes code and follows certain rules to avoid overwriting developer-written code that may be written after previous code generation steps.

Software and Hardware Integration and Allocation of Software Components to Platform and Hardware Resources

AADL Analysis

Using AADL as the modeling framework for HAMR allows developers to utilize a variety of AADL-based model analysis that complement code generation and support broader system engineering activities. Some of the analyses most commonly used with HAMR are:

• Model-based hazard analysis using AADL’s Error Modeling Annex and supporting analyses

• Information flow analysis that uses AADL’s flow annotations

• Timing and scheduleability analyses with tools like Adventium’s FASTAR that work off of AADL’s timing annotations and thread properties

• Component behavior specification (e.g., component contracts) and verification using tools such as AGREE and BLESS

Typical workflows will likely use some AADL analyses before generating code (these may generate additional information, e.g., properties using scheduling analysis, that code generation may utilize), while other analyses may be used after code generation or during repeated code generation steps.

Information Flow Analysis

Awas information flow analysis (awas.sireum.org) generates scalable interactive visualizations of AADL information flows and model-based hazard analysis results. Given an AADL model with information flow annotations, Awas will generate a Javascript/HTML5 browser-based visualization of the models information flow that you can dynamically browse and query with path logic.

Awas information flow analysis is an example of the synergistic interplay between HAMR code generation and AADL analyses – HAMR code generation for communication infrastructure ensures that inter-component information flows as visualized by Awas are actually preserved (no new flow paths are added) in the executable system (note: this does not consider various side channels).

Awas provides scalable visualizations of information flow specified in AADL modeling

Awas works by generating an internal information flow graph derived from the declared connections between components in the AADL model (capturing inter-component flows) and AADL component flow annotations (capture intra-component flows – flows between a component’s input and output ports).

In the current state of the tooling, AADL flows for intra-component flows must be written by hand (one can think of this as “modeling” the component implementation’s information flow) and there is no checked correspondence between AADL flow declarations and the source code of AADL component. Adventium Labs and Kansas State have an Phase II SBIR grant from AFRL to develop (a) automatic inference of AADL flows from Slang implementations of components, as well as support for a complementary workflow in which hand-written AADL flows (serving as information flows specifications) are automatically checked against information flows found in Slang component implementations, ensuring that information flow in the Slang component implementations conforms to the AADL flow specifications.

Note that the code generation in the current tooling guarantees correspondence between the model-level inter-component information flows (represented as component connections) and the code-level information flow reflected in port-based inter-component communication. This correspondence is not formally proven correct at this time.

Awas dependence graphs are derived (in part) from developer-specified AADL intra-component flow annotations

The figure above illustrates AADL intra-component flow specifications and their corresponding representations in the Awas-generated Javascript visualizations. For example, given an AADL process component MC_SW, AADL flow specifications can be used to specify that information flows from the position_status input port to the send_status output port. The Awas tabular view of component inputs and outputs at the bottom of the figure provides a summary of the input/output and information flow aspects of a component. Awas query results are displayed using coloring to mark up particular set of inputs and outputs and flows that participate in a resulting information flow path.

Awas provides interactive information flow querying (e.g., via clickable graphical representations) and visualizations of query results

The figure above illustrates how Awas can simultaneously display information flow of multiple subsystems or multiple levels of the system hierarchy. Awas support multiple forms of queries. In the example above, in the display for the top-level components in the system architecture, the user clicks on an output port (with a forward information flow option being previously set), and Awas immediately calculates and visualizations the connections, ports, and components in the system that may receive information derived from the outputs of the selected port. In this example, the query corresponds to the application concern “how does map information propagation from ground station to UAV and through UAV’s mission computer to produce a waypoint?”.

An extended walk-through of Awas browsing and querying can be found at this link .

Slang Workflows

This section provides an overview of HAMR capabilities that are used when developing components implementations using Slang and executing a system on the JVM platform.

Generating Code and Code Development Environment Setup in the IntelliJ-based Sireum Integrated Verification Environment (Sireum IVE)

Once the AADL model has been developed to a level of detail sufficient to support code generation, the HAMR code generation capability can be invoked from the OSATE menu system.

HAMR Code Generation (Slang / JVM Platform)

HAMR generates code for:

• communication infrastructure code that implements communication between AADL threads (e.g., communicating over port connections),

• threading infrastructure code for containers that host threads and a thread component state (one for each thread instance in the AADL model),

• code skeletons for thread application code,

• build scripts (in SBT) for configuring a build of the system and identifying needed library packages,

• unit testing infrastructure that aids the developer in setting up unit tests for each thread component,

• code that supports simulation and visualization of Slang systems.

The developer will subsequently implement the system by filling in the code skeletons for the application code, configuring build scripts, adding unit and system tests, etc. The generated infrastructure code is complete and should not be modified in the development process.

For programming component logic, the workflow transitions from the Eclipse-based OSATE AADL environment (or the DARPA CASE customized version of OSATE called the FMIDE) to the IntelliJ-based Sireum Integrated Verification Environment (Sireum IVE). HAMR installation instructions cover the installation of both the FMIDE and Sireum IVE. The Sireum IVE extends IntelliJ with extensions to the Scala compiler and other facilities used to support Slang. When using HAMR’s C-based workflows, there is a similar handoff from OSATE/FMIDE to C IDE’s such as JetBrain’s CLion.

HAMR Workflow Transition from OSATE/FMIDE (for AADL) to Sireum IVE (for Slang/Scala/Java)

Within the Sireum IVE, the different types of code generated by HAMR are structured in a hierarchy of files/packages. The developer’s primary concern will be the AADL component implementation code, AADL data type implementations, and unit and system tests. A HAMR beginner usually doesn’t need to understand the details of the other types of files.

HAMR Slang Code Organization in the Sireum IVE (IntelliJ IDE)

Build Scripts

HAMR generates generates default build scripts in SBT. SBT is similar to Maven and Ant – popular Java-oriented build tools. For example, SBT adopts Maven’s project folder structure and supports library dependences in Apache IVY library repositories.

However, SBT builds are defined in a Scala data structures (as opposed to XML used in Maven and Ant), and this provides greater flexibility, some degree of type checking on build definitions (utilizing underlying type checking facilities of Scala), and a deeper integration with the Scala ecosystem.

The HAMR-generated SBT build script is sufficient for running the initial default behavior of the HAMR-generated system and for launching auto-generated example unit tests.

Developers extend the default build scripts as needed to specify library dependences and to tailor execution and testing workflows for the application.

Component Development

HAMR generates code skeletons for AADL thread components. For each thread, the structure of the thread’s skeletons depends on the dispatch protocol (periodic, sporadic, etc.) selected in the AADL definition of thread.

Note

Add figure for component code skeletons.

The skeleton for each thread includes a default implementation consisting some simple logging commands and illustrations of how to use port APIs. The default implementations enable the generated code to be immediately executed. The default implementations can be replaced incrementally with complete implementations – all the while maintaining a system that can be executed.

When completing a thread implementation, the developer will typically (a) use the auto-generated port APIs to read data from input ports, (b) code the “business logic” that works on thread inputs and other component local variables, and (c) use the auto-generated port APIs to write data to output ports.

HAMR Slang Complement Implementation (AADL Thread Components)

The figure aboves shows part of the component implementation (the event handler for the tempChanged input event port in TempControl component).

Note

Add figure for extensions and GUI components.

System Development and Execution

HAMR build scripts integrate component implementations with auto-generated communication and threading infrastructure to produce an executable system. System execution can be started using an auto-generated launcher that can be launched within the Sireum IVE. Logging information is displayed in the console of the Sireum IVE.

HAMR Slang Launcher and Basic Execution with Logging in Sireum IVE

Unit Testing

• IMAGE (need to draw): Explanation of component testing in terms of component inputs and outputs

• Illustration of code providing inputs and checking outputs

• Running via Scala Test

System Testing

• System testing via controlled schedule exploration

System Monitoring and Execution Visualization

• Inspector Framework

• MSC Visualization

• Redis logging

C Workflows

Generating Code and Code Development Environment Setup

• Screen shot of OSATE menu (explain multiple platform options)

• Quick overview of generated code in CLion IDE

• Setting up builds with CMAKE

Component Development

• Coding component logic

• Reading and writing from ports

• Interfacing with Java and component GUIs

Scheduling and System Configuration

• Configuring scheduler

Linux System Execution

• illustration of Linux Execution

seL4 System Execution (simulation via Qemu)

• illustration of seL4 Execution on Qemu

seL4 System Execution (on development board)

• illustration of seL4 Execution on board