HAMR Installation¶

Overview¶

HAMR is supported on Windows, Linux, and MacOS platforms.

Using HAMR to build an executable system requires working with:

• FMIDE (Formal Methods Integrated Development Environment) – a customization of the Eclipse-based OSATE AADL IDE created on the DARPA CASE project. The FMIDE includes the HAMR code generation plugin.

• 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.

The Sireum Kekinian framework is used to ease the installation of these tools and associated infrastructure. Kekinian is installed first, and then its installation scripts are used to install the FMIDE and Slang and C development environments.

As part of the DARPA CASE project, Vagrant scripts are provided to build a VirtualBox VM running Linux that hosts the tool components above.

Following the installation instructions, instructions are given for loading and running a simple HAMR Slang project.

Installing and Updating FMIDE (customization of AADL OSATE IDE) and HAMR¶

• Windows:

  git clone https://github.com/sireum/kekinian Sireum
  cd Sireum
  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
  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
  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.

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 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