In this course you will be introduced to best practices for the application of formal methods, a set of mathematically rigourous techniques for the formal specification, validation, and verification of safety- and security-critical cyberphysical systems, of which aircraft and spacecraft are the prime example. We will explore the tools, techniques, and applications of formal methods, focusing on the aerospace domain.
We will examine the latest research to gain an understanding of the current state of the art, including the capabilities and limitations of applying formal methods for systems analysis. Students will leave with a better understanding of real-world system specification, design, and verification, including why the FAA specifically calls out formal methods in certification requirements such as DO-178B, DO-178C, and DO-254, and why modern security teams from DARPA to AWS require formal methods for cloud security.
This course is intended to be a fun, interactive introduction to applying
formal analysis in the context of real-world systems. Hands-on learning, through the use of software tools
in homeworks and projects, will be emphasized. We will learn the real tools used at NASA, Boeing, Rockwell Collins, Honeywell, Airbus, Amazon, and others. Students from all
areas of aerospace engineering, electrical and computer engineering, computer science,
cybersecurity, mathematics, and other engineering disciplines, are
encouraged to enroll.
The prerequisite is mathematical maturity: Calculus II plus familiarity with discrete mathematics (or ability to learn them quickly from review material made available in the course). This prerequisite take the form of a disjunction; one of the following is required: AERE 361, COMS 311, or permission of the instructor.
Do not struggle with tool installation on your own machine! If you are running linux, these tools should all install easily, but if not, use the provided virtal machines. There is no credit for time spent trying to install a tool. To access tools like spin, you will need to vpn in from off campus and then ssh -X email@example.com. This works from a command line (e.g., in linux), or from mobaXterm in windows. All software (e.g., Isabelle and nuXmv) is installed in /usr/local/packagename, except for spin and ispin, which are in /usr/local/bin. The GUI ispin is invoked by running "ispin.tcl" from the command line. Nathan Vaughn also wrote a blog post about how to get ispin working with windows
Exam Dates (estimated)
Final Project: (in lieu of final exam)
Optional GitHub classroom link:
Project Midterm Report:
11/5 or 11/10 Give short mid-term presentations on this day!
Friday Progress Reports Due:
11/12, 11/19, 11/26 (optional), 12/3, 12/10
During exam period (9:45am-11:45am on Monday, 12/13)
Homework 0 due 8/26
Homework 1 due 9/2
Homework 2 due 9/14
Homework 3 due 9/30
Homework 4 due 10/7
Homework 5 due 10/14
Homework 6 due 10/21
Choice of research paper for in-class presentation due 10/19
Homework 0 (Review of Version Control and LaTeX primer): distributed 8/24 from
Note: if you want a deeper understanding of git, there are many online courses.
Homework 1 (Propositional Logic Review): distributed 8/26 from
- There is an appendix with additional definitions here.
Homework 2 (Temporal Logic): distributed 9/2 from
Homework 3: distributed 9/14 from
Homework 4: distributed 9/30. Submit
Homework 5: distributed 10/7. Submit
Homework 6: distributed 10/14. Submit
Choice of research paper for presention due via email: 10/19
You may not choose a paper authored by the professor.
Professor evaluation form for in-class presentations is available HERE
Student evaluation form for in-class presentations is available HERE
Here is some great advice on How to Give a Good Research Presentation.
Here is some great advice on How to Read a Paper (there is also advice on how to write papers).
Paper Presentation Schedule:
Each presentation should be approximately 25 minutes, including time for questions.
|10/26|| Midterm Examination|
|10/28|| & & |
|11/ 2|| & & |
|11/ 4|| & & |
|11/ 9||Midterm project report presentations|
|11/11||Midterm project report presentations|
|11/16|| & & |
|11/18|| & & |
|11/30|| & & |
|12/2|| & & |
|12/6||Final project report presentations|
|12/9||Final project report presentations|
|12/13||(during final exam period) Final project report presentations|