Development of High-Assurance Software Systems

The course will cover techniques for developing high assurance systems -- systems that are safety critical, security critical, or mission critical in nature. In contrast to general purpose systems, high assurance system development tends to place a more stronger emphasis on rigorous requirements and specifications, verification and validation, risk management, and certification. High assurance system development is more likely to be amenable to and benefit from formal verification techniques -- techniques that use various forms of machine-checkable mathematics or logic to demonstrate that a system satisfies its specification. The goal of this course teach techniques for developing critical software that would usually not be covered in other courses in your computer science degree program. In particular, the course will focus on writing requirements for safety critical systems, formal architecture definition, risk management techniques including various forms of hazard analysis, safety systems, and automated verification. We will aim to illustrate an end-to-end development process for critical systems using examples of varying size.

Some quick pointers for navigating this site:

  • Use the tabs in the top tool bar to see different material supporting the course.
  • Lectures -- contains lecture slides, lecture videos, and links to relevant reading materials
  • Projects -- contains supporting material for course projects including the Patient Controlled Analgesic (PCA) Pump medical device project
  • Tools -- contains links to various modeling and analysis tools used in the course
  • Syllabus -- contains administrative details for students interested in taking the course

If you are a faculty member or student at another university and you end up using this material in some way, I (John Hatcliff) would very much appreciate it if you would let me know. It's beneficial for me and our research group to be able to report such uses to agencies that fund our work.

Acknowledgements:This material is based upon work supported by the National Science Foundation under Grants # 0734204, 0930647, 0932289, 1065887, 1238431, 1239543, 1239324 by an National Institutes of Health NIBIB Division grant via a subcontract from the Medical Device Plug-n-Play Interoperability Program (MDPnP) at the Center for the Integration of Medicine and Innovative Technology (CIMIT), and by the Air Force Office of Scientific Research.

Thanks to Brian Larson, Kim Fowler, and Sam Procter for making significant contributions to the lecture materials and artifacts used in this course.