Instructor: Professor Kristin Yvonne Rozier

E-mail: kyrozier@iastate.edu

Office: 2335 Howe Hall

Office hours:
12:40pm--1:55pm or by appointment

Postdoctoral Lecturer: Dr. Jianwen Li

Email: ?@iastate.edu

Office: TBD Howe Hall

Office hours: by appointment

Guest Lecturer: Rohit Dureja

Email: dureja@iastate.edu

Office hours: by appointment

Location: Howe Hall 0620-E

Meeting Time: TR 11:00am--12:15pm


AERE/COMS 407X/507X
Applied Formal Methods

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 safety-critical 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.

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, 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

Spin Model Checker

http://spinroot.com/
nuXmv Model Checker
https://es-static.fbk.eu/tools/nuxmv/
PVS Theorem Prover
http://pvs.csl.sri.com/
PRISM Model Checker
http://www.prismmodelchecker.org/
Dafny Language and Program Verifier
http://rise4fun.com/dafny/
Z3 SMT Solver
https://github.com/Z3Prover/z3
CBMC (Bounded Model Checker for C and C++ programs)
http://www.cprover.org/cbmc/
Coq Proof Assistant
https://coq.inria.fr/
Book: Formal Reasoning About Programs



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 on-campus or connected to the VPN from off-campus 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: 10/19
-- Review for midterm on 10/17; send any questions for review to the professor by 10/16 at the latest

Final Project: (in lieu of final exam)

Project Requirements: HERE
Optional git classroom link: HERE
Project Proposal: 10/17
Project Midterm Report: 11/9 Give short mid-term presentations on this day!
Project Presentations: 12/5: 12/7:
Friday Progress Reports: 11/3, 11/10, 11/17, 11/24, 12/1
Final Report: During exam period (9:45am-11:45am, Monday, Dec. 11, 2017)

Reading/Homeworks

Homework 0 (Review of Version Control and LaTeX primer): distributed 8/22 from HERE

Homework 1 (Propositional Logic Review): distributed 8/24 (in-class handout). Submit HERE

  • There is an appendix with additional definitions here.

Homework 2: distributed 8/29 (in-class handout). Submit HERE

Homework 3: distributed 9/?. Submit HERE

Homework 4: distributed 9/?. Submit HERE

Homework 5: distributed 9/?. Submit HERE

Homework 6: distributed 10/?. Submit HERE


Choice of research paper for presention due via email: 10/?

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 Read a Paper.

Paper Presentation Schedule:
Each presentation should be approximately 30 minutes, including time for questions.

10/24? & ?
10/26? & ?
10/31? & ?
11/2TBD
11/7? & ?
11/9Midterm project report presentations
11/14TBD
11/16TBD
11/28? & ?
11/30? & ?
12/5Final project report presentations
12/7Final project report presentations

Assignment Deadlines

Homework 0 due ?

Homework 1 due ?

Homework 2 due ?

Homework 3 due ?

Homework 4 due ?

Homework 5 due ?

Homework 6 due ?

Choice of research papaer for in-class presentation due ?

Optional Textbooks

Use this for:
  • good background on LTL: well-formed 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 non-standard
  • 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, deadlock-freeness, fairness
  • overview of modeling abstraction methods
  • out-of-date 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

Links
Research
Blog
Publications
Home