TCCOE 2022 HAMR seL4 Tutorial¶
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.
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)
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.
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.