Course Summary
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 safetycritical 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 realworld system specification, design, and verification, including why the FAA specifically calls out formal methods in certification requirements such as DO178B, DO178C, and DO254.
This course is intended to be a fun, interactive introduction to applying
formal analysis in the context of realworld systems. Handson 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, and others. Students from all
areas of aerospace engineering, electrical and computer engineering, computer science,
and other engineering disciplines, are
encouraged to enroll.
Course Syllabus
Tools
You may either install these tools on your local machine or run them on ISU's remote linux servers. The tools can be run via a remote desktop connection (e.g., ssh Y X) to linuxremote1.engineering.iastate.edu thru linuxremote4.engineering.iastate.edu. You must be oncampus or connected to the VPN from offcampus to reach these systems. For example, 'spin' and 'ispin' run from the command line. These applications are installed in /opt/Spin. All of the examples, documentation, etc. can be found there. PVS and nuXmv are also available on the linux remote servers.
Exam Dates
Midterm: 3/9
 Review for midterm on 3/7; send any questions for review to the professor by 3/6 at the latest
Final Project: (in lieu of final exam)
Project Requirements:

HERE

Optional git classroom link:

HERE

Project Proposal:

3/21

Project Midterm Report:

4/11 Give short midterm presentations on this day!

Project Presentations:

4/25: Swarn, Shruti, Emily, Ahilan

4/27: Michael, Brian, Avinash+Chandan, Shravan

Friday Progress Reports:

3/24, 3/31, 4/7, 4/14, 4/21

Final Report:

During exam period (9:45am11:45am, May 2, 2017)

Reading/Homeworks
Homework 0 (Review of Version Control and LaTeX primer): distributed 1/10 from HERE
 Regrades for Homework 0 due on 1/19 via the same link.
Homework 1 (Propositional Logic Review): distributed 1/17 (inclass handout). Submit HERE
 There is an appendix with additional definitions here.
Homework 2: distributed 1/24 (inclass handout). Submit HERE
Homework 3: distributed 1/31. Submit HERE
Homework 4: distributed 2/9. Submit HERE
Homework 5: distributed 2/21. Submit HERE
Homework 6: distributed 2/28. Submit HERE
Choice of research paper for presention due via email: 3/9
Professor evaluation form for inclass presentations is available HERE
Student evaluation form for inclass presentations is available HERE
Here is some great advice on How to Read a Paper.
Paper Presentation Schedule:
Each presentation should be approximately 30 minutes.
3/21  Michael & Swarn 
3/23  Shruti & Shravan 
3/28  Emily & Brian 
3/30  Rockwell Collins Guest Lecture 
4/4  Chandan & Avinash 
4/6  Ahilan 
4/11  Midterm project report presentations 
4/13  Guest Lecture 
4/18  Guest Lecture 
4/20  Guest Lecture 
4/25  Final project report presentations 
4/27  Final project report presentations 
Assignment Deadlines
Homework 0 due 1/12
Homework 1 due 1/24
Homework 2 due 1/31
Homework 3 due 2/9
Homework 4 due 2/16
Homework 5 due 2/28
Homework 6 due 3/7
Choice of research papaer for inclass presentation due 3/9
Optional Textbooks

Use this for:
 good background on LTL: wellformed formulas, semantics, encoding English sentences, expressivity, normal forms, relationship to automata
 reactive system properties: safety, liveness, fairness
 specification and modeling of real systems
 deciding the truth of a temporal formula; related proof techniques including explicit model checking
 thorough chapter on Spin, including how to run it from the command line and a good Promela tutorial
 review of classical and propositional logic
 extensions including synthesizing software from specifications
Be cautious that:
 LTL is instead called PTL in this book; that is nonstandard
 LTL2BA is not the best tool; SPOT is far superior now: https://spot.lrde.epita.fr/
 URLs provided are outdated (no longer active or superseded by the state of the art)
 Spin chapter refers to outdated xspin (though only briefly)


Use this for:
 supplemental material on temporal logics (LTL, CTL, CTL*)
 background on automata as system models
 review of explicit and symbolic model checking
 reachability, safety, liveness, deadlockfreeness, fairness
 overview of modeling abstraction methods
 outofdate chapters on SPIN and SMV still have useful reviews of basic tool usage
 ideas for related formal methods, including timed automata models, additional tools
Be cautious that:
 This book is extremely out of date!
 LTL is the proper name for Linear Temporal Logic (book calls it PLTL)
 comparisons of LTL vs CTL/CTL* have been changed/been disproved
 SMV version described is no longer available; current tool is nuXmv
 Spin version described has been updated (xspin vs ispin)

LaTeX Resources

