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


(content will appear here throughout the semester)

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, Part 3 .pdf)

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)


  • 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


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

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


  • 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)


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

Disaster Cast Podcast


  • 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)


  • Introduction to Medical Application Platforms

Slang Embedded

Lecture: Slang Embedded Tool Chain Overview

This lecture presents an overview KSU SAnToS Lab’s Slang Embedded tool chain for developing high-assurance embedded systems. The tool includes a component modeling and analysis layer based on the AADL modeling framework, code generation, development, and simulation using Slang (a safety-critical subset of Scala), and code generation to C for various micro-kernel and separation platforms. Other lectures will “drill down” into the details of each of the tool chain elements.

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 (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)