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:
Throughout the presentation, forward references are provided to subsequent chapters that provide more details.
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 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.
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
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
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 a port category (together with optional port properties) indicates a particular pattern of communication to be used for communication on that port.
dataports – roughly correspond to shared memory between components that act either as writers or readers
eventports – roughly corespond to buffered notifications from one component to another
event dataports – 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
out), so as to enable (a) clean design of security and information flow controls and (b) model- and code-level information flow analysis.
Later in the workflow, HAMR will generate code-level interfaces for modeled component types.
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.
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.
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
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.
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 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.
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.
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 .
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 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.
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 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.
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.
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.
The figure aboves shows part of the component implementation (the event handler for the
tempChanged input event port in
Add figure for extensions and GUI components.
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.
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 via controlled schedule exploration
Screen shot of OSATE menu (explain multiple platform options)
Quick overview of generated code in CLion IDE
Setting up builds with CMAKE
Coding component logic
Reading and writing from ports
Interfacing with Java and component GUIs
illustration of Linux Execution
illustration of seL4 Execution on Qemu
illustration of seL4 Execution on board