HAMR Installation¶
Overview¶
These instructions assume that you have read through the HAMR Overview and HAMR Tour material.
HAMR supports model-based system development using multiple programming languages including Slang and C. Systems can be created for execution on multiple platforms. The HAMR tool chain itself can be installed on Windows, Linux, and MacOS platforms.
The programming language and system execution platform that you choose determines the tools that you will work with and the workflows that you will follow.
The HAMR Workflows video and slides on the HAMR Videos page illustrate possible HAMR workflows and installation options.
In general, using HAMR to build an executable system requires working with:
The Eclipse-based OSATE or OSATE customization FMIDE (Formal Methods Integrated Development Environment) for creating AADL models and invoking HAMR code generation. We recommend using the FMIDE because the HAMR plug-in is already installed in it. If you are using AADL for other purposes and already have OSATE installed (perhaps with other plug-ins added), you can install the HAMR plug-in directly.
A development environment for the HAMR targeted programming language(s) – the programming language used to code the implementation of components whose skeletons and associated run-time infrastructure are generated by HAMR. HAMR currently supports Slang (a Scala-based language), C, with some support for CakeML. Currently, HAMR support for Slang is the most mature and easy-to-use. When coding components in Slang, you will need to install the Sireum IVE (Integrated Verification Environment) customization of the IntelliJ IDE – which will support you in coding/debugging Slang with extensions in Scala and Java. When coding components in C, you will need to install a C IDE that can process CMake files. We recommend using the JetBrains CLion IDE. However, other IDEs such as Microsoft Visual Studio Code can also be used.
Execution platform support - HAMR systems can be built for JVM, Linux/Mac OSX based operatoring systems, and the seL4 microkernel running in the Qemu simulator or on a development board.
There are at least two approaches to installing the tool chain elements above:
install them directly, with assistance from Sireum Kekinian framework. Kekinian is installed first, and then a few simple command line options can be used to install the FMIDE, Sireum IVE, JVM, etc. This is recommended when you are working with Slang and JVM deployments, and it is also suitable for C-based development on Linux.
install them via a virtual machine built using the Vagrant VM build tool - As part of the DARPA CASE project, Vagrant scripts are provided to build a VirtualBox VM running Debian Linux that hosts the tool components above. If you are working with seL4 or if you are working with DARPA CASE technologies and examples, it is strongly recommended that you install the HAMR tool chain using the Vagrant VM scripts.
The following describes the most common HAMR workflows and recommended installation approaches. These workflows are described in greater detailed in the video and slides available on the HAMR Videos page.
Component development using the Slang programming language with system deployment on the JVM - Tools used include the Eclipse-based OSATE or FMIDE (OSATE customization) for creating AADL models, Sireum IVE (IntelliJ customization) for coding and running Slang. The workflow can be set up on Mac OSX, Linux, or Windows. The preferred way to install is to download the Sireum Kekinian framework and use it to install the necessary components. Alternatively, you can use the DARPA CASE Vagrant VM building infrastructure to build a virtual machine running Debian with all the required tools installed.
Component development using the C programming language with system deployment on Linux/MacOS X - Tools used include the Eclipse-based OSATE or FMIDE (OSATE customization) for creating AADL models, and CLion IDE for coding and running C (other C IDEs can be used as well). The preferred way to install is to use the DARPA CASE Vagrant VM building infrastructure to build a virtual machine running Debian with all the required tools installed. Alternatively, you can download Sireum Kekinian and use it to install the required tools directly in Linux or Mac OSX.
Component development using the C programming language with system deployment on seL4 micro-kernel - Tools used include the Eclipse-based OSATE or FMIDE (OSATE customization) for creating AADL models, and CLion IDE for coding and running C (other C IDEs can be used as well), and multiple components from Data61 for working with seL4. The preferred way to install is to use the DARPA CASE Vagrant VM building infrastructure to build a virtual machine running Debian with all the required tools installed. Alternatively, you can download Sireum Kekinian and use it to install the required tools directly in Linux or Mac OSX. You will also need to download and install the Data61 tools for seL4.
Following the installation instructions, instructions are given for loading and running a simple HAMR Slang project.
Installation Option: Direct Installation with Assistance from the Sireum Kekinian Framework¶
Installing and Updating FMIDE (customization of AADL OSATE IDE) and HAMR¶
You will first install SAnToS Lab Sireum Kekinian programming language tools, and then use that to install the FMIDE for creating AADL models and performing HAMR code generation.
Windows:
git clone https://github.com/sireum/kekinian Sireum cd Sireum git submodule update --init --recursive bin\build.cmd setup bin\install\fmide.cmd start /B bin\win\fmide\fmide.exe
Linux:
git clone https://github.com/sireum/kekinian Sireum cd Sireum git submodule update --init --recursive bin/build.cmd setup bin/install/fmide.cmd bin/linux/fmide/fmide&
macOS:
git clone https://github.com/sireum/kekinian Sireum cd Sireum git submodule update --init --recursive bin/build.cmd setup bin/install/fmide.cmd open bin/mac/fmide.app
The Sireum directory created above is referred to using the environment variable $SIREUM_HOME in the instructions below.
Occassionally, the FMIDE will be updated to include new HAMR code generation or AADL analysis capabilities. To update the FMIDE, simply re-run the FMIDE install script as illustrated below.
Windows:
%SIREUM_HOME%\bin\install\fmide.cmd
Linux/macOS:
$SIREUM_HOME/bin/install/fmide.cmd
If the installation somehow did not finish (e.g., due to a network issue), remove the problematic file in Sireum’s cache directory (~/Downloads/sireum) and re-run the above.
Updates to the Sireum framework may add new code-level verification, analysis, and compilation functionality. When you update Sireum, you should update the FMIDE as well.
To update Sireum and the FMIDE, with your current directory as $SIREUM_HOME, simply do a git pull with –recurse-submodules option, and re-run build.cmd setup and fmide.cmd, e.g., for macOS this would be
git pull --recurse-submodules
bin/build.cmd setup
bin/install/fmide.cmd
Note that it is also possible to download specific versions (specific git commit tips) for both Sireum and the FMIDE. For details, see https://github.com/sireum/case-env.
IDE (Sireum IVE) for Slang-based Development of HAMR Systems¶
When using Slang to program an AADL/HAMR based system, you will use the Sireum IVE (Integrated Verification Environment). Sireum IVE is a customization of IntelliJ that includes Scala-associated infrastructure pre-installed as well as other SAnToS-built plug-ins for the Slang language subset and associated analysis/verification capabilities.
The Sireum Kekinian framework is used to install and update the Sireum IVE. Thus, Sireum IVE is installed as part of the steps above.
Then, to launch it:
Windows:
start /B %SIREUM_HOME%\bin\win\idea\bin\IVE.exe
Linux:
$SIREUM_HOME/bin/linux/idea/bin/IVE.sh&
macOS:
open $SIREUM_HOME/bin/mac/idea/IVE.app
IDE for C-based Development of HAMR Systems¶
Any C modern IDE can be used. The HAMR team uses CLion from JetBrains.
To install and run CLion C/C++ IDE (license required/free 30-day evaluation):
Windows:
%SIREUM_HOME%\bin\install\clion.cmd start /b %SIREUM_HOME%\bin\win\clion\bin\clion64.exe
Linux:
$SIREUM_HOME/bin/install/clion.cmd $SIREUM_HOME/bin/linux/clion/bin/clion.sh&
macsOS:
$SIREUM_HOME/bin/install/clion.cmd open $SIREUM_HOME/bin/mac/clion/CLion.app
Installation Option: Vagrant VM-based Installation¶
Follow the instructions from DARPA CASE Github repository. Vagrant scripts are provided to build a VirtualBox VM running Debian Linux that hosts the tool components above as well as tools supporting development for seL4. The VM also includes other CASE analysis and model transformation tools.