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.
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
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.
Software and Hardware Integration and Allocation of Software Components to Platform and Hardware Resources
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.
Tour-HAMR-code-generation-JVM .. _HAMR-code-generation-JVM:
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.
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.
ToDo: Add screenshot of SBT file:
Coding component logic (e.g., temp controller with port reads and writes)
Reading and writing from ports
Interfacing with Java and component GUIs
Test edit of HAMR tour under component development. Foo bar
Component integration and scheduling, with concept of running on platform (perhaps with HAMR image of platform)
Console logging information
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
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