Week of Lectures Assignments

  1. Jan 18

  • Lecture: Course Overview
  • Lecture: Sets and Relations
  • Lecture: Isolette Example
  • Install: Alloy 5.1.0

  1. Jan 25

  • Lectures: Alloy Tour (a, b, c)

  1. Feb 1

  • Lectures: Alloy Tour (d, e)
  • Lecture: Introduction to AADL Component-based System Architecture

  • Project 1: Basic Alloy (due Feb 15)

  1. Feb 8

  • Lectures: Alloy Logic (b, c)

  1. Feb 15

  • Lectures: Alloy Logic (d, e)

  • Project 2: Advanced Alloy (due Mar 8)

  1. Feb 22

  • Exam: Alloy

  1. Mar 1

  • Install: Sireum IVE
  • Reading: End-to-End Formal Methods Integrated Development with SysMLv2 using HAMR
  • Reading: The Sireum Programming Language

  1. Mar 8

  • Lecture: HAMR Code Generation

  • Reading: HAMR: An AADL Multi-Platform Code Generation Toolset
  • Project 3: HAMR Code Generation (due Mar 29)

  1. Mar 15

  • Spring Break

  1. Mar 22

  • Lecture: HAMR GUMBO

  • Reading: An AADL Contract Language Supporting Integrated Model- and Code-Level Verification

  1. Mar 29

  • Lecture: HAMR seL4

  • Project 4: HAMR GUMBO (due Apr 12)
  • Reading: seL4: Operating Systems With The Reliability of Mathematics
  • Reading: Verus: A Practical Foundation for Systems Verification

  1. Apr 5

  • Lecture: Introduction to Logika

  • Reading: Logika: The Sireum Verification Framework – An Overview

  1. Apr 12

  • Lecture: Logika Basics

  • Project 5: Logika (due Apr 26)

  1. Apr 19

  • Lecture: Advanced Logika

  1. Apr 26

  • Lecture: Testing Framework

  • Project 6: Advanced Logika (due May 10)

  1. May 3

  • Lecture: Wrap-up

  1. May 10

  • No final exam