Week. Meeting: Date Lectures/Lab

  1. T: Aug 20

  • Course Overview
  • Sets and Relations
  • Install: Alloy 5.1.0

  1. U: Aug 29

  • Alloy Tour (a, b, c)
  • Quiz 1: Sets and Relations

  1. U: Sep 5

  • Alloy Tour (d, e)
  • Project 1: Alloy (due Sep 25)
  • Quiz 2: Alloy Tour (a, b, c)

  1. U: Sep 12

  • Alloy Logic (b, c)
  • Quiz 3: Alloy (d, e)

  1. T: Sep 17

  • Alloy Logic (d, e)
  • Quiz 4: Alloy Logic (b, c)

  1. U: Sep 26

  • Airport Example (a, b)
  • Project 2: Alloy (due Oct 20)
  • Quiz 5: Alloy Logic (d, e)

  1. U: Oct 3

  1. T U: Oct 8 & 10

  • Exam 1 Discussion
  • Introduction to SysMLv2 and HAMR
  • GUMBO Contract

  1. U: Oct 17

  1. U: Oct 24

  • Isolette Intro (Canvas; also see FAA REMH)
  • Project 3: SysMLv2, HAMR, and GUMBO (due Nov 10)

  1. T U: Oct 29 & 31

  • HAMR Code Generation (seL4)
  • Isolette
  • Exam 2: SysMLv2, HAMR, and GUMBO

  1. T U: Nov 5 & 7

  • Exam 2 Discussion
  • HAMR Testing Framework [FMICS23, NFM24]
  • Introduction to Logika

  1. T U: Nov 12 & 14

  • Logika: Methods and Loops
  • Project 4: Logika (due Dec 8)
  • Quiz 7: Methods and Loops

  1. T U: Nov 19 & 21

  • Logika: Sequences and Termination
  • Quiz 8: Sequences and Termination

  1. Thanksgiving Break

  1. T U: Dec 3 & 5

  • Logika: Rewriting System

F. Dec 9: 2-3:50pm

  • Final Exam