HAMR Videos¶
Overview¶
This page lists various support videos for HAMR, including
overview videos
installation and use tutorials
lecture videos from high-assurance systems and embedded courses that cover AADL and HAMR
Note: most of these videos are hosted on Google Drive. We have observed that these Google-hosted videos sometimes fail to launch in certain web browers. If this happens for you, we suggest that you use the Google Chrome browser, as we have found it to be the most reliable for launching these Google-hosted videos.
Overview Videos¶
HAMR Overview (with emphasis on Slang language development) - (video) (around 1 hr plus additional time for questions)
This talk was given at CMU Software Engineering Institute in July 2019 as part of the SEI Director’s Lecture Series. The talk reports on HAMR’s role in the SEI/KSU funded research project called ISSE - Integrated Safety and Security Engineering. The talk covers general motivation for model-driven development using HAMR in avionics, mission control, and medical domains, basics of the HAMR code generation architecture, code examples of programming HAMR-generated components using Slang (a safety-critical subset of Scala developed by KSU), illustration of various simulation capabilities for HAMR/Slang systems running on the JVM. This talk emphasizes HAMR’s Slang/JVM platform backend.
HAMR for Applications built on the seL4 Microkernel (with emphasis on C language development) (video (25 minutes), slides)
This was an invitated presentation given at the November 2020 seL4 Summit. The presentation begins with an overview of how HAMR facilitates the development of applications built on the seL4 micro-kernel and how it complements existing seL4 development tools by providing a systems engineering-focused model-driven development environment. It then illustrates aspects of HAMR C-centric workflows being used on the DARPA CASE project. It provides simple code examples that illustrate programming AADL components in C, and explains how HAMR component application code in C can be deployed on both Linux and seL4 platforms. It concludes with a short demo illustrating deployment and execution of a HAMR-built system on both Linux and seL4.
Installation and Use Tutorials¶
HAMR Workflow Overview - (video (~35 minutes), slides)
HAMR supports multiple platforms and multiple programming languages. The programming language and platform that you choose to work with determines the tools that you will work with and the workflows that you will follow. This video provides an overview of different HAMR workflows and indicates which tools will be involved for each workflow. This video assumes that you have read through the HAMR Overview and HAMR Tour material.
The video identifies the following basic workflows:
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 (explained in the video below). 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 and use it to install the required tools directly in Linux or Mac OSX (explained in the video below).
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 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 (explained in the video below).
The video also describes several more advanced workflows that combine Slang and C development and address migrating HAMR system implementations across multiple platforms.
HAMR Installation - (video (~3 minutes))
This video covers the downloading and installation of HAMR. The video demonstrates installation on Linux, but steps for Windows and MacOS platforms are almost identical. For written installation instructions, see HAMR Installation.
HAMR C Workflow Overview - (video (~9:30 minutes))
This video provides an overview of the workflows for creating an AADL model, invoking the HAMR code generator, implementing component behaviors in C, and deploying and executing the system on Linux and seL4 (Qemu-based simulation). This video is meant to be an quick overview of the workflows. Details for AADL modeling and coding HAMR-generated components in C are provided in subsequent videos.
HAMR C Component Implementation Details - (video (~9:50 minutes))
This video provides details on implementing in C the application logic for AADL HAMR-generated components. Basic aspects of working with HAMR C type structures, APIs for reading and writing values on ports, and debugging information are presented.
Lecture Videos and Supporting Material¶
The High Assurance Systems graduate course at Kansas State University provides in-depth lectures on AADL modeling and HAMR development using Slang. The course material is being updated for the Spring 2021 semester, and relevant videos and slides will be linked from here as they become available.