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