Lectures

Course Administration

Safety Critical Systems Concepts

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: Differences between Conventional Development and Development of Safety-Critical Systems

Lecture: Basic Safety-Related Terminology

  • Slides: (pdf)
  • Reading: Hatcliff et al. “Certifiably Safe Software-Dependent Systems: Challenges and Directions”, Future of Software Engineering 2014, at the International Conference on Software Engineering (Sections 1,2.1) (pdf)
  • Study Guide: (txt)

HAMR / AADL / SysMLv2

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)

This is a two 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.

Part 1: Provides the overall motivation and scope for HAMR, and covers how HAMR uses AADL.

Part 2: Illustrates programming HAMR-generated components/systems in Slang (a high-assurance subset of Scala), which can be integrated with Scala and Java and deployed on the JVM (or alternatively, pure Slang can be compiled to C). This lecture also illustrates a variety of HAMR/Slang-related capabilities such as unit testing, run-time monitoring, and fault injection.

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.

  • Video (mp4)
  • Example Files: Use HAMR-Slang-Tutorials-Example-00.zip from above. If you have already downloaded, no need to download again.

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.

  • Exercise instructions (online readme)
  • Example Files: Use the OSATE import of the HAMR-Slang-Tutorials-Example-00.zip from above.
  • Solution explanation video: (mp4)

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 Proyek build system 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).

Solution explanation video: (mp4)

  • 0:00 - Overview
  • 15:23 - Loading AADL and Slang projects from provide zip file (optional – only needed if you are not starting from the results of previous exercises)
  • 19:48 - Confirming code is ready for exercise; hints about what will change in code; building existing project before refactoring
  • 23:04 - Explanation of how code generation avoids overwriting existing application files but does generate new infrastructure files
  • 26:06 - Code Generation
  • 38:54 - Compile and Observe Errors
  • 40:42 - Refactor the TempSensor Compute Entry Point Code
  • 44:30 - Refactor the TempSensor Initialize Entry Point Code
  • 48:18 - Recompile and Observe Errors (some eliminated)
  • 45:50 - Refactor the Message Handlers in the TempControl Compute Entry Point
  • 55:55 - Recompile and Observe Errors (more eliminated)
  • 57:20 - Refactor the OperatorInterface Compute Entry Point
  • 59:08 - Recompile (No Errors)
  • 59:50 - Refactor TempControl Unit Tests
  • 1:03:40 - Run Unit Tests
  • 1:04:40 - Run System

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.

Solution explanation video: (mp4)

  • 0:00 - Overview
  • 7:43 File System - HAMR Project Directory Hierarchy Creation
  • 11:52 OSATE - AADL New Project Creation
  • 16:39 Discussion: Top-down vs Bottom-up Model Creation
  • 18:22 OSATE - Creation of Producer Package Skeleton
  • 27:04 OSATE - Creation of ProdCons (system-level) Package and Message Data Type
  • 32:50 OSATE - Creation of Producer Artifacts
  • 37:55 Discussion: OSATE Content Assist
  • 50:05 OSATE - Creation of Consumer Artifacts
  • 56:00 OSATE - Creation of System Component
  • 1:01:45 OSATE - Instance Model Creation
  • 1:03:48 OSATE - Diagram Creation

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”.

Solution explanation video: (mp4)

  • 0:00 - Overview, Background, and Preparation
  • 4:10 - Ensure that the file system has the proper structure for a HAMR Slang project
  • 6:43 - Confirm AADL Model is Ready for Slang Code Generation
  • 8:03 - Generate Code (and explanation of structure of HAMR Slang generated code (around 13:22))
  • 17:58 - Open Slang Project in the Sireum IVE (IntelliJ)
  • 20:42 - Compile
  • 22:40 - Run Skeleton Code
  • 23:50 - Discussion: Explanation of Behavior of Skeleton Code (with intuition about AADL semantics)
  • 32:37 - Provide Slang Declarations of Producer Component Local State Variables (with discussion about understanding/using the Slang types generated from AADL types, special formatting of literals)
  • 47:25 - Implement Producer Initialize Entry Point (with discussion of standard structure for initialize entry point: initializing component local variables, and putting initial values on output data ports)
  • 54:04 - Implement Producer Compute Entry Point (with discussion of calling constructors for Slang representations of AADL-derived types, using output port APIs, using Slang if-statements, other AADL entry points)
  • 1:09:08 - Compile and Run (with explanation of logging output when we have a completed producer but are still using the auto-generated template for the consumer)
  • 1:12:43 - Provide Slang Declarations of Consumer Component Local State Variables
  • 1:15:18 - Implement Consumer Initialize Entry Point
  • 1:15:57 - Implement Consumer Compute Entry Point (with a discussion of the semantics of AADL HAMR event handlers around 1:17:45, discussion of example API usage 1:20:54, discussion of coding the entry point 1:22:50)
  • 1:29:17 - Compile and Run (with a discussion of understanding the output of the completed system)
  • 1:31:37 - Conclusion

Requirements Engineering

General Reading FAA Requirements Engineering Management Handbook (pdf)

Lecture: Introduction to Requirements

  • Slides: (.pdf)
  • Video: (.mov)

Lecture: FAA REMH Overview

  • Slides: (.pdf)
  • Video: (.mov)

Lecture: FAA REMH: System Overview

  • Slides: (.pdf)
  • Video: (.mov)
  • Supplement: Advice and common pitfalls (.pdf,.mov)

Lecture: FAA REMH: Identify the System Boundary

  • Slides: (.pdf)
  • Video: (.mov)

Lecture: FAA REMH: Develop the Operational Concepts

  • Slides: (.pdf)
  • Video: (.mov)

Lecture: Additional material on details of use case writing based on Cockburn’s Writing Effective Use Cases Action Steps

  • Slides: (.pdf)
  • Video: (.mp4)

Extensions

  • Slides: (.pdf)

Lecture: FAA REMH: Identify the Environment Assumptions

  • Slides: (.pdf)
  • Video: (.mov)

Lecture: FAA REMH: Develop the Functional Architecture

  • Slides: (.pdf)
  • Video: (.mov)

Lecture: FAA REMH: Revise the Functional Architecture to Meet Implementation Constraints

  • Slides: (.pdf)

Lecture: FAA REMH: Identify the System Modes

  • Slides: (.pdf)

Lecture: FAA REMH: Develop Detailed Requirements

  • Slides: (.pdf)

Lecture: FAA REMH: Define the Software Requirements

  • Slides: (.pdf)

Disaster Cast Podcast

The Disaster Cast podcast by safety engineer Drew Rae is an execellent source for interesting stories and intuitive explanations of safety-related concepts. Unfortunately, the podcast is a bit old now, and the original website seems to be unavailable. However, the files have been snarfed up by several podcast websites. For example, you can find the recordings at this link.

The links below organize a selection of the podcasts into phases; I have selected some that I found especially interesting or that convey important concepts that I think should be emphasized in this course. The overviews of for each phase linked below include instructions for how I would like you to listen to and take some simple notes on the podcast episodes.

Disaster Cast Phase 1

  • See here for instructions for the first phase of disaster cast podcasts.