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:
There are at least two approaches to installing the tool chain elements above:
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.
Following the installation instructions, instructions are given for loading and running a simple HAMR Slang project.
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
REM The following step is optional -- only needed it you want to check out a particular commit tip
REM Otherwise, proceed directly to git submodule update ...
git checkout <commit> & REM^; SHA commit of https://github.com/sireum/kekinian, see SIREUM_V in case-setup.sh; optional step
git submodule update --init --recursive
bin\build.cmd setup
bin\install\fmide.cmd [<tag-name>] & REM^; Optional release tag name; latest nightly release is used if unspecified
start /B bin\win\fmide\fmide.exe
Linux:
git clone https://github.com/sireum/kekinian Sireum
cd Sireum
# The following step is optional -- only needed it you want to check out a particular commit tip
# Otherwise, proceed directly to git submodule update ...
git checkout <commit> # SHA commit of https://github.com/sireum/kekinian, see SIREUM_V in case-setup.sh; optional step
git submodule update --init --recursive
bin/build.cmd setup
bin/install/fmide.cmd [<tag-name>] # Optional release tag name; latest nightly release is used if unspecified
bin/linux/fmide/fmide&
macOS:
git clone https://github.com/sireum/kekinian Sireum
cd Sireum
# The following step is optional -- only needed it you want to check out a particular commit tip
# Otherwise, proceed directly to git submodule update ...
git checkout <commit> # SHA commit of https://github.com/sireum/kekinian, see SIREUM_V in case-setup.sh; optional step
git submodule update --init --recursive
bin/build.cmd setup
bin/install/fmide.cmd [<tag-name>] # Optional release tag name; latest nightly release is used if unspecified
open bin/mac/fmide.app
The Sireum directory created above is referred to using the environment variable $SIREUM_HOME
in the instructions below.
To update FMIDE,
Windows:
%SIREUM_HOME%\bin\install\fmide.cmd [<tag-name>] & REM^; Optional release tag name; latest nightly release is used if unspecified
Linux/macOS:
$SIREUM_HOME/bin/install/fmide.cmd [<tag-name>] # Optional release tag name; latest nightly release is used if unspecified
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.
To update Sireum, simply do a git pull, recursively update its submodules, and re-run build.cmd setup and fmide.cmd.
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
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
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.