Lecture: Course Administration
This lecture provides a slide-based walkthrough of the course syllabus. It describes the course policies, means of delivering course content, evaluation methods, grading scale, etc.
Lecture: Control Loop Basics illustrated with Temperature Controller Example
This lecture introduces concepts associated with “control loops” – a foundational concept in the design and implementation of embedded systems and safety-critical systems. A control loop consists of the “real-world thing” that the system is trying to control (the controlled process), the controller (i.e., software/hardware that makes decisions about how to control the controlled process), sensors (used by the controller to get “readings” the real-world state of the controlled process), and actuators (used by the controller to change the state of the controlled process in some way). The lecture briefly discusses how requirements engineering and safety reasoning relate to control loops.
Lecture: AADL Overview
This presentation by Dr. Sam Procter from the Software Engineering Institute describes AADL, its use in industry, and some of the ongoing research projects that AADL. NOTE: Dr. Procter is a PhD graduate from SAnToS Lab/KSU, and he first learned about AADL in this course!
Lecture: AADL: Modeling Embedded Software
This lecture covers the basic aspects of modeling embedded software with AADL using the temperature controller example. The lecture includes concepts related to AADL thread, process, and system components, AADL port-based communication, and AADL packages. The lecture scope is tailored to the subset of AADL supported by HAMR code generation. This material provides the basis for follow-on tool tutorials that use the AADL OSATE environment to develop simple system software models.
Lecture: HAMR Overview (Parts 1, 2, 3)
This is a three part lecture that provides an overview of the HAMR model-driven development tool for AADL (HAMR stands for “High Assurance Modeling and Rapid Engineering for Embedded Systems”). This lecture should be watched before moving on to other HAMR-related lectures.
Tool Tutorial: HAMR Installation
This video covers installation of the HAMR tool following the options of a direct install (as opposed to the virtual machine option) and using the Formal Methods Integrated Development Environment (FMIDE) customization of the OSATE AADL editor (as opposed to installing HAMR in the “regular” OSATE distribution). Instructions for other types of installation can be found on the HAMR website. Also, this video addresses installation of the tools needed for Slang development of HAMR-generated components. The HAMR website explains how to extend this installation with the tools needed for C development of HAMR-generated components.
Tool Tutorial: AADL OSATE Workspace Concepts
The OSATE AADL editor is based on Eclipse, and it uses the Eclipse “workspace” concept to manage AADL project files. This video gives an overview of the workspace concept and recommendations for how to use workspaces in the context of HAMR development. You should follow these recommendations when working with HAMR AADL models in this tutorial series.
Tool Tutorial: Loading an Existing AADL Project into OSATE/FMIDE
You will often (in the course of these lectures/tutorials or in the course of team development) be given an existing AADL project to work with in the OSATE AADL editor. This tutorial explains how you load existing AADL projects into OSATE and it illustrates some basic OSATE navigation of an AADL model.
Tool Tutorial: Loading an Generated/Existing HAMR Slang Project into the IntelliJ-based Sireum IVE
Given an AADL model, HAMR can generate a HAMR Slang project with AADL run-time infrastructure and component code skeletons that you add application code to to get a complete system. This video explains how you open a HAMR Slang project in the Sireum IVE (a customization of IntelliJ). These instructions also apply to opening existing HAMR Slang projects that are distributed in the HAMR Slang tutorials. The tutorial addresses the basic structure of HAMR Slang projects, notes the use of the Scala Build Tool (SBT) to manage project builds, describes basic correspondences between HAMR generated Slang code and AADL models, describes how to compile and run a HAMR Slang project, how to run unit tests. The tutorial concludes with an initial discussion of project files that should be not checked into git and other source code repositories.
Tool Exercise: Refactoring an AADL Model to Remove Ports and Change Port Categories
This is an exercise designed for you to complete on your own following the provided instructions. A solution video is provided that is meant to be used help you resolve any difficulties encountered when trying to do the exercise on your own.
In this exercise, you will carry out a simple refactoring of some of the component ports in the Temperature Control example. You will start from the AADL model in the HAMR-Slang-Tutorials-Example-00.zip that you imported into OSATE in the tutorials above. This refactoring will involve changing the kinds of ports and connections used to communicate temperature information from the sensor to the controller (and to the operator interface). This will require changing the AADL thread component types for TempSensor , TempController , and OperatorInterface components, as well as making some simple changes to corresponding AADL flow specifications. By performing this refactoring, you will gain an initial understanding of (a) AADL architecture models (basic ideas of ports and connections) and (b) using the OSATE editor to make simple edits in the AADL graphical and textual views.
Tool Exercise: Refactoring a Slang Implementation of an AADL System
This is an exercise designed for you to complete on your own following the provided instructions. A solution video is provided that is meant to be used help you resolve any difficulties encountered when trying to do the exercise on your own.
This exercise is designed to help you learn the basics of using HAMR to generate Slang implementations of AADL-based systems, Slang thread component application logic, and Slang port-communication APIs.
In this exercise, you will carry out a simple refactoring of some of the Slang application code in the Temperature Control example. This builds on a refactoring of the original Temperature Control AADL model carried out in a previous exercise. In that exercise you changed the kinds of ports and connections used to communicate temperature information from the sensor to the controller (and to the operator interface). In this exercise, you will regenerate the Slang code from the refactored AADL model. This will keep most of the existing code, but it will change the Slang APIs associated with your component ports to align with the refactored models. This will leave the Slang code with some syntax errors because the old application code will not completely match the newly regenerated APIs for port communication. To address this, you will then need to make some small changes in the Slang component application code to match the new version of the generated port APIs. You will confirm that your refactored code is working correctly by compiling and running it with the SBT build file in IntelliJ.
This exercise is meant to start from the state of your AADL models and Slang code from previous exercises. However, if you don’t have your files in a proper state, the .zip file below contains both AADL models and Slang code in the correct state for starting the exercise. You will need to import these files into OSATE and Sireum IVE (see the exercise description).
Tool Exercise: Creating an AADL Model from Scratch
This is an exercise designed for you to complete on your own following the provided instructions. A solution video is provided that is meant to be used help you resolve any difficulties encountered when trying to do the exercise on your own.
In this exercise, you will create an AADL model of a simple producer/consumer system. This will cover creation of AADL packages (with imports), threads, processes, systems, and a struct-based data type. The solution video also illustrates the OSATE content assist facility and creation of AADL graphical model diagrams from the completed textual model.
To assist you in completing this exercise and subsequent AADL modeling activities, you are provided with a collection of AADL templates (in a text file) that you can cut/paste into OSATE using your favorite text editor.
Tool Exercise: Creating a HAMR Slang Project from Scratch
This is an exercise designed for you to complete on your own following the provided instructions. A solution video is provided that is meant to be used help you resolve any difficulties encountered when trying to do the exercise on your own.
In the previous exercise “Creating an AADL Model from Scratch”, you created an AADL model of a simple producer/consumer system. In this exercise, you will build a Slang-based implementation of the system that will run on the JVM. This will help you learn how to prepare your directory structure for HAMR Slang code generation, invoke the HAMR code generator to generate Slang code from an AADL model, code simple application logic (for the Producer and Consumer threads, in this example), and compile and run the system.
This exercise is meant to start from the state of your AADL models in the previous “Creating an AADL Model from Scratch” exercise. However, if you don’t have your files in a proper state, the HAMR-Slang-Tutorials-Prod-Cons-AADL-only.zip file below contains AADL Producer/Consumer model (essentially the model-solution for the previous exercise). These are in the correct state for starting the exercise. You will need to import these files into OSATE following the steps that you took in the exercise “Loading an Existing AADL Project into OSATE/FMIDE”.
Lecture: Isolette - Introduction
This lecture introduces concepts related to Isolette infant incubator medical device.
Lecture: Isolette - Architecture
This lecture provides an overview of the AADL-based Isolette Architecture.
Lecture: PCA Pump - Introduction
This lecture introduces concepts related to PCA Pump medical devices.
Lecture: PCA Pump - Open PCA Pump Architecture
This lecture provides an overview of the AADL-based Open PCA Pump Architecture.
The lectures from previous semesters are provided below as a resource.