Lectures

CS 855: Development of High-Assurance Software Systems

Course Administration

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: Course Overview

This lecture provides an overview of the course content, homework themes, and course projects.

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.

AADL

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.

HAMR - A model-driven development environment for embedded systems that uses AADL

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.

  • 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.
  • Part 3: Illustrates programming HAMR-generated components/systems in C for deployment on Linux or the seL4 micro-kernel.
  • Slides (Part 1 .pdf, Part 2 .pdf)
  • Video (Part 1 .mp4, Part 2 .mp4)

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 (.pdf)
  • 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 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).

  • Exercise instructions (.pdf)
  • .zip file artifacts starting point: (.zip)
  • Solution explanation video: (.mp4)
    • 0:00 - Overview
    • 21:26 - Code Generation
    • 30:06 - Compile and Observe Errors
    • 32:38 - Refactor the TempSensor Initialize Entry Point Code
    • 35:46 - Refactor the TempSensor Compute Entry Point Code
    • 39:48 - Recompile and Observe Errors (some eliminated)
    • 40:37 - Refactor the Message Handlers in the TempControl Compute Entry Point
    • 51:25 - Recompile and Observe Errors (more eliminated)
    • 52:08 - Refactor the OperatorInterface Compute Entry Point
    • 58:32 - Recompile (No Errors)
    • 59:20 - Refactor TempControl Unit Tests
    • 1:03:25 - Run Unit Tests
    • 1:06:39 - 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.

  • Exercise instructions (.pdf)
  • AADL Template File: (.txt)
  • 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”.

  • Exercise instructions (.pdf)
  • .zip file artifacts starting point: (.zip)
  • 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

Lectures from Previous Semesters

The lectures from previous semesters are provided below as a resource.


Course Overview and Introduction to Safety Concepts

  • Isolette: A Simple Safety Critical System
  • Differences between Conventional Development and Development of Safety-Critical Systems
    • 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 (Section 2.2) (.pdf)
  • 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)

Requirements Management for Safety Critical Systems

General Reading

  • FAA Requirements Engineering Management Handbook (.pdf)

Lectures

  • Introduction to Requirements
  • FAA REMH Overview
  • FAA REMH: System Overview
  • FAA REMH: Identify the System Boundary
  • FAA REMH: Develop the Operational Concepts
    • Slides: (.pdf)
    • Video: (.mov)
    • Additional lecture slides on details of use case writing based on Cockburn's Writing Effective Use Cases
  • FAA REMH: Identify the Environment Assumptions
  • FAA REMH: Develop the Functional Architecture
  • FAA REMH: Revise the Functional Architecture to Meet Implementation Constraints
  • FAA REMH: Identify the System Modes
  • FAA REMH: Develop Detailed Requirements
  • FAA REMH: Define the Software Requirements

PCA Pump Project

Lectures

  • PCA Pump -- Introduction
  • PCA Pump -- Architecture Overview

Modeling Safety-Critical Systems in the Architecture and Analysis Definition Language (AADL)

Lectures

  • Modeling the Isolette in AADL

Risk Management

General Reading

  • "Basic Concepts and Taxonomy of Dependable and Secure Computing", Algirdas Avizienis, Jean-Claude Laprie, Brian Randell, and Carl Landwehr (.pdf)
  • "Architecture Fault Modeling and Analysis with the AADL Error Modeling Annex v.2", Peter Feiler John Hudak Julien Delange David P. Gluch (.pdf)
  • "Illustrating the AADL Error Modeling Annex (v. 2) Using a Simple Safety-Critical Medical Device", Brian Larson, John Hatcliff, Kim Fowler, Julien Delange (.pdf)

Lectures

  • AADL EMv2 -- Introduction
  • AADL EMv2 -- Error Types and Library

Disaster Cast Podcast

Instructions

  • Instructions for Disaster Cast notes (.txt)

Medical Application Platforms

General Reading

  • John Hatcliff, Andrew King, Insup Lee, Alisdair Macdonald, Anura Fernando, Michael Robkin, Eugene Vasserman, Sandy Weininger, Julian Goldman. "Rationale and Architecture Principles for Medical Application Platforms", Proceedings of the 2012 International Conference on Cyber-Physical Systems, pp. 3-12, April, 2012. (.pdf)

Lectures

  • Introduction to Medical Application Platforms

STM32 and FreeRTOS

Exercise: STM32 Tool Chain Installation and Blinking LED

This exercise guides you through the installation of development tools for STM32F4 Discovery Boards and construction of a simple FreeRTOS task to blink one of the LEDs built into the Discovery board.

Arduino

Arduino (Elegoo) Mega 2560 Tutorials

This 225-page document provides 33 exercises to help you learn how to program all of the different widges that come with the Arduino (Elegoo) Mega 2560 kit that is required for the course (you can purchase the kit from Amazon).

  • Tutorial Document (.pdf)