TCCOE 2022 HAMR seL4 Tutorial

Overview

This page presents the artifacts used in the TCCOE tutorial

• tutorial slides and videos

• virtual machine file (.ova) that provides a virtual machine for the tools and example files used in the tutorial

Note: most of these artifacts 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.

Slides and Videos

HAMR Overview (slide presentation) (slides, video) Provides an overview of the HAMR framework and objectives for the tutorial

AADL Concepts and Tutorial Example (slide presentation) (slides, video) Provides an overview of the subset of AADL used by HAMR and presents the example system used in the tutorial.

Demo: Launching tools in provided VM, Editing AADL models in OSATE (video)

Demo: Running Resolint to Check AADL Model Well-formedness for HAMR (video)

Demo: Invoking HAMR Code Generation (video)

Demo: Opening Generated Code in CLion and Running Template Code (video)

HAMR Generated Code Overview (slide presentation) (slides, video) Provides an overview of the execution semantics of HAMR-generated systems, a description of the code skeletons generated, a description of the auto-generated APIs for port-based communication, and an overview of the AADL Data Modeling framework as used by HAMR.

Demo: Overview of Auto-Generated Code Skeletons (video)

Demo: Walkthrough of Generated Data Types (video)

Demo: Coding Application Logic, Running on Linux (video)

HAMR seL4 Backend (slide presentation) (slides, video) Provides a brief overview of how HAMR generates seL4-specific artifacts including CAmkES and AADL adapter code for seL4, and how the seL4 domain scheduler is used to provide static scheduling.

Demo: Deploying Application on SeL4 using QEMU (video)

Conclusions and Future Development Goals for HAMR (slide presentation) (slides, video) Describes ongoing projects and future directions for HAMR.

Virtual Machine Setup and Tutorial Artifacts

The instructions for downloading and setting up the VM for the tutorial can be found here .

An OVA (Open Virtual Appliance) has been created that has all the development tools that will be used in this tutorial preinstalled. You will need a virtualization provider that is capable of importing the OVA such as VMWare or VirtualBox. We recommend using VirtualBox as it is free/open-source and can be downloaded via https://www.virtualbox.org/wiki/Downloads

All the tools and examples needed for the tutorial are included in the VM.

Other Lecture Videos and Supporting Material

The High Assurance Systems graduate course at Kansas State University provides in-depth lectures on AADL modeling (including the lectures/exercises suggested for learning AADL) and HAMR development using Slang.