CPSC 513 Winter 2009-2010 Term 1 Class Home Page

Integrated Systems Design:

Introduction to Formal Verification


Contents of this page


Growing Set: avi mpg
Final Set: avi mpg


Late Breaking News:


Handouts

Hard copies are not distributed in class -- if you want one, print it.

# Date Topic
1 Monday, October 6 Guidelines for Reading & Reviewing Papers
2 Wednesday, October 14 Course Project Overview
3 Wednesday, November 18 Course Project Presentations
3 Monday, November 30 Course Project Final Reports


Homeworks

Homework Submission Policy:

Topic Due Date Assignment Assignment Links Solution Solution Links
Hybrid & Continuous Systems December 14 Problem Set None. None. None.

Course Overview

What this course is not: The official title "Integrated Systems Design" of CPSC 513 is an historical misnomer. The course is actually about formal verification of systems constructed from computer hardware, software or some combination of both. The course content has been redirected for two reasons. First, more professors in the department are working in verification than in design. Second, demand from industry for graduates skilled in verification techniques is outstanding.

What this course is: An introduction to formal verification, so that students can get an overview of the field. Evaluation will be a combination of homeworks, paper presentations and a course project. The course should be approachable and applicable to students throughout computer science. Students interested in pursing further study and research of formal verification will be equipped to work with and/or take advanced courses from the ISD professors (Mark Greenstreet, Alan Hu and Ian Mitchell).

This course shares a fair amount of content with the most recent previous CPSC 513 offerings: 2008-2009 (taught by Ian Mitchell) and 2007 (taught by Alan Hu).

Motivation: A central feature of modern design methods is the modeling and simulation of the system as early and as often as possible, since models and simulations are usually much cheaper, faster and safer to construct than physical prototypes. However, for many complex systems the costs and challenges of exhaustive simulation have become overwhelming.

The field of formal verification uses mathematical reasoning about system models to draw conclusions about system behavior without exhaustive simulation. It has been applied to systems including:

  • The analog propagation of charge through wires and transistors of integrated circuits.
  • The digital operation of arithmetic/logic units and register files in computer chips.
  • Communication protocols for caches and computer networks.
  • Integrated hardware/software embedded systems in consumer electronics.
  • Collision avoidance procedures for vehicles such as cars and aircraft.
  • Small but critical software services such as operating system device drivers.

While of particular interest in safety critical systems -- such as the computers which maintain the stable flight of modern aircraft -- formal methods have also found fertile ground in applications where they can more quickly and/or cheaply provide test coverage than simulation based approaches.

Topics (in brief):With so many different application areas, it is not surprising that this field draws on many sub-disciplines of computer science, engineering and mathematics. In the limited time available, this course will touch only on a subset of the formal verification field, including:

  • Models of computation for concurrent, real-time, continuous and hybrid systems.
  • Formal methods of specification, abstraction and refinement.
  • Conceptual tools such as invariants, reachability, fixpoint iteration, weakest precondition and assume/guarantee.
  • Algorithms and implementations such as binary decision diagrams (BDDs), satisfiability, symbolic model checking, automated theorem proving and Lyapunov functions.

Expectations: In addition to attending lectures, students will:

  • Read and discuss academic papers.
  • Complete several homework assignments involving both paper and pencil and programming components.
  • Complete a project involving some aspect of formal verification. The project will include a proposal, a presentation and a brief written report.



Course Details

Intended Audience: Graduate students in

Prerequisites: Graduate standing or consent of the instructor.

Grades: Your final grade will be based on a combination of:

The relative weighting will depend on how many homeworks you do.

Instructor: Ian Mitchell

Lectures: 12:30 - 14:00, Mondays and Wednesdays, ICCS 238.

References: There is no textbook for the course. Readings will come from original research papers listed (and linked) in the Schedule below. Background and additional material can be found in the Links below, or in the following books:


Topics and Readings

Date Topic Links Required Readings Optional Readings
Sept 9 Introduction. Introduction slides (including syllabus handout). Ariane 5 failure video and accident report. Website listing famous software bugs. Leah Hoffman, "In Search of Dependable Design" in Communications of the ACM, vol. 51, num. 7, pp. 14-16 (July 2008). Leah Hoffman, "Q&A: Talking Model Checking Technology" in Communications of the ACM, vol. 51, num. 7, pp. 110-112 (July 2008).
Sept 14 A taste of hybrid system reachable sets. STARMAC backflip video demonstrating an application of backward reachable sets. None. None.
Sept 16 A (rather dated) view of computer aided verification. None. Edmund M. Clarke & Robert P. Kurshan, "Computer-Aided Verification" in IEEE Spectrum, June 1996, pp. 61-67 None.
Sept 21 Introduction to Systems with State. Markov Assumption. Wikipedia entries for State transition system and Markov process. Randal E. Bryant, "A View from the Engine Room: Computational Support for Symbolic Model Checking" in 25 Years of Model Checking (Orna Grumberg & Helmut Veith, eds.), LNCS 5000, pp. 145-149 (2008). R. P. Kurshan, "Verification Technology Transfer" in 25 Years of Model Checking (Orna Grumberg & Helmut Veith, eds.), LNCS 5000, pp. 46-64 (2008). None.
Sept 23 Finite Automata. Well-posed systems: deadlock/blocking, nondeterminism. None. David L. Dill, Andreas J. Drexler, Alan J. Hu & C. Han Yang, "Protocol Verification as a Hardware Design Aid" in ICCD Proceedings, pp. 522-525 (October 1992). None.
Sept 28 Concurrent systems. Guarded Command Languages. Murphi and examples. Murphi package for explicit state model checking. David L. Dill, "A Retrospective on Murphi" in 25 Years of Model Checking (Orna Grumberg & Helmut Veith, eds.), LNCS 5000, pp. 77-88 (2008). None.
Sept 30 Class cancelled
Oct 5 Invariants. Reachable Sets by Explicit State Enumeration. Examples of Symmetry and its Role in Murphi. Wikipedia entries for equivalence relation, simulation and bisimulation. C. Norris Ip & David L. Dill, "Better Verification through Symmetry" in International Conference on Computer Hardware Description Languages, pp 87-100 (April 1993) C. Norris Ip & David L. Dill, "Better Verification through Symmetry" in Formal Methods in System Design, Volume 9, Numbers 1/2, pp 41-75 (August 1996) -- This is the long, formal and precise version of the required paper.
Oct 7 Murphi wrap-up. Introduction to Software Verification. None. Mike Hinchey et al, "Software Engineering and Formal Methods", Communications of the ACM, vol. 51, num. 9, pp. 54-59 (September 2008). John C. Mitchell, Mark Mitchell, & Ulrich Stern, "Automated analysis of cryptographic protocols using Murphi" in IEEE Symposium on Security and Privacy, pp.141-151 (May 1997).
Oct 12 No Class (Thanksgiving)
Oct 14 Two Examples of Software Verification Tools: SLAM and Astrée. SLAM toolkit, specifically developed for Windows device driver verification, but can be generalized. Astrée Static Analyzer. Thomas Ball & Sriram K. Rajamani, "Automatically Validating Temporal Safety Properties of Interfaces", Proc. SPIN Workshop on Model Checking of Software, pp. 103-122 (2001). Laurent Mauborgne, "Astrée: Verification of Absence of Runtime Error", Building the Information Society (R. Jacquard, ed), pp. 385-392 (2004). David Delmas & Jean Souyris, "Astrée: From Research to Industry", Static Analysis Symposium (H. Riis Nielson and G. Filé, eds.), LNCS 4634, pp. 437-451 (2007). Bruno Blanchet et. al, "A static analyzer for large safety-critical software", Conference on Programming Language Design and Implementation, pp. 196-207 (2003). Patrick Cousout et. al., "The Astrée Analyzer", European Symposium on Programming (M. Sagiv, ed.), LNCS 3444, pp. 21-30 (2005).
Oct 19 Abstract interpretation: The theory behind Astrée. Note: class starts at 13:00. Wikipedia entry for abstract interpretation. The Wikipedia entry and Patrick Cousot, "Abstract Interpretation Based Formal Methods and Future Challenges", Informatics: 10 Years Back, 10 Years Forward (Reinhard Wilhelm, ed.), LNCS 2000, pp. 138-156 (2001). Patrick Cousot, "Abstract Interpretation: Achievements and Perspectives", SSGRR 2000 Computer & eBusiness International Conference, compact disk paper 224 (2000) (Good paper, but obscure venue). Patrick Cousot & Radhia Cousot, "Basic Concepts of Abstract Interpretation", Building the Information Society (R. Jacquard, ed), pp. 385-392 (2004).
Oct 21 More software verification: Java Pathfinder Java PathFinder (JPF). The readings and many other papers can also be found at this site. Willem Visser et al, "Model Checking Programs" in Automated Software Engineering, v. 10, n. 2, pp. 203-232 (April 2003). Guillaume Brat et al, "Experimental Evaluation of Verification and Validation Tools on Martian Rover Software", Formal Methods in System Design, v. 25, n. 2-3, pp. 167-198 (September 2004). Klaus Havelund & Thomas Pressburger, "Model checking JAVA programs using JAVA PathFinder", Int. J. Software Tools for Technology Transfer, v. 2, n. 4, pp. 366-381 (March 2000).
Oct 26 Continuous and Hybrid Dynamical Systems. Interactive Education Modules in Scientific Computing: Ordinary Differential Equations (online material for Heath's book). John Polking's pplane software for phase plane plots of ODEs. Lygeros notes chapters 1, 2. Lygeros citations.
Oct 28 Well-posed Differential Equations. Hybrid Time Trajectories. Hybrid Trajectories and Executions. Classes of Hybrid Systems. Well-posed Hybrid Systems. Wiki page collecting tools for hybrid systems (both simulation and verification). Lygeros notes chapter 3, 4 Lygeros citations.
Nov 2 Reachability Algorithms for Continuous Systems: Lagrangian Schemes with Polytopes and Zonotopes. Lecture slides for both lecture 13 & 14 (4.7 MB). CheckMate. MATISSE. PHAVer. d/dt. Alongkrit Chutinan & Bruce H. Krogh, "Computing polyhedral approximations to flow pipes for dynamic systems" in Proceedings of IEEE International Conference on Decision and Control (Tampa, FL), pp. 2089-2094 (1998). Antoine Girard, "Reachability of Uncertain Linear Systems Using Zonotopes" in Hybrid Systems Computation & Control (Manfred Morari & Lothar Thiele eds), LNCS 3414, pp. 291-305 (2005). Alongkrit Chutinan & Bruce H. Krogh, "Computational techniques for hybrid system verification" in IEEE Transactions on Automatic Control, vol. 48, num. 1, pp. 64-75 (2003). Eugene Asarin, Olivier Bournez, Thao Dang & Oded Maler, "Approximate Reachability Analysis of Piecewise-Linear Dynamical Systems" in Hybrid Systems Computation & Control (Nancy Lynch & Bruce H. Krogh eds.), LNCS 1790, pp. 20-31 (2000). Eugene Asarin, Thao Dang, Goran Frehse, Antoine Girard, Colas Le Guernic & Oded Maler, "Recent Progress in Continuous and Hybrid Reachability Analysis" in IEEE International Symposium on Computer-Aided Control Systems Design (Munich, Germany), pp. 1582-1587 (2006).
Nov 4 Reachability Algorithms for Continuous Systems: Lagrangian Schemes with Ellipsoids and Projectagons. Lecture slides for both lecture 13 & 14 (4.7 MB). Ellipsoidal Toolbox. Alexander B. Kurzhanski & Pravin Varaiya, "Ellipsoidal Techniques for Reachability Analysis" in Hybrid Systems Computation & Control (Nancy Lynch & Bruce H. Krogh eds.), LNCS 1790, pp. 202-214 (2000). Mark R. Greenstreet & Ian Mitchell, "Reachability Analysis Using Polygonal Projections" in Hybrid Systems Computation & Control (Frits W. Vaandrager & Jan H. van Schuppen, eds.), LNCS 1569, pp. 103-116 (1999). Alex A. Kurzhanskiy & Pravin Varaiya, "Ellipsoidal Toolbox (ET)" in Proceedings of IEEE International Conference on Decision and Control (San Diego, CA), pp. 1498-1503 (2006). Oleg Botchkarev & Stavros Tripakis, "Verification of Hybrid Systems with Linear Differential Inclusions Using Ellipsoidal Approximations" in Hybrid Systems Computation & Control (Nancy Lynch & Bruce H. Krogh eds.), LNCS 1790, pp. 73-88 (2000). Chao Yan & Mark R. Greenstreet, "Circuit Level Verification of a High-Speed Toggle" in Proceedings of Formal Methods in Computer Aided Design (Austin, TX), pp. 199-206 (2007).
Nov 9 Comparing Forward and Backward Reachability. Comparing Reachability Slides (3.6 MB). Ian M. Mitchell, "Comparing Forward & Backward Reachability as Tools for Safety Analysis" in Hybrid Systems Computation & Control (Alberto Bemporad, Antonio Bicchi & Giorgio Buttazzo eds.), LNCS 4416, pp. 428-443 (2007). None.
Nov 11 No Class (Remembrance Day)
Nov 16 Reachable Sets for Nonlinear Systems with Inputs: Eulerian Schemes using Hamilton-Jacobi and Viability Methods. Eulerian Reachability slides (3.2 MB). The Toolbox of Level Set Methods. Claire J. Tomlin, Ian M. Mitchell, Alexandre M. Bayen & Meeko Oishi, "Computational Techniques for the Verification of Hybrid Systems" in Proceedings of the IEEE, volume 91, number 7, pp. 986-1001 (July 2003). Lygeros notes chapter 7. Ian M. Mitchell, Alexandre M. Bayen & Claire J. Tomlin, "A Time-Dependent Hamilton-Jacobi Formulation of Reachable Sets for Continuous Dynamic Games" in IEEE Transactions on Automatic Control, volume 50, number 7, pp. 947-957 (July 2005).
Nov 18 Temporal Logics: CTL, LTL and CTL*. None. E. M. Clarke, E. A. Emerson & A. P. Sistla, "Automatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications" in ACM Trans. Programming Languages, volume 8, number 2, pp. 244-263 (April 1986). We will not go into the details of the alternating bit protocol. E. Allen Emerson & Joseph Y. Halpern, "'Sometimes' and 'Not Never' Revisited: On Branching versus Linear Time Temporal Logic" in Journal of the ACM, volume 33, number 1, pp. 151-178 (January 1986). A discussion of differences between CTL, CTL* and LTL.
Nov 23 Determining the Existence of DC Operating Points in Circuits. Guest Lecturer Mohammed Zaki. Lecture slides. HySAT tool. INTLAB tool. EigTool and the Pseudospectral Gateway. Mohammed H. Zaki, Ian M. Mitchell & Mark R. Greenstreet, "DC Operating Point Analysis -- A Formal Approach", Formal Verification of Analog Circuits Workshop, Grenoble, France (June 2009). None.
Nov 25 Extended Static Checking for Java (presented by Robin Salkeld). Timed automata and bisimulation. None. Cormac Flanagan et. al, "Extended Static Checking for Java" in Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 234-245 (2002).

Lygeros notes chapter 6.
K. Rustan M. Leino, "Extended Static Checking: A Ten-Year Perspective", Informatics: 10 Years Back, 10 Years Forward (Reinhard Wilhelm, ed.), LNCS 2000, pp. 157-175 (2001). Rajeev Alur & David L. Dill, "A Theory of Timed Automata" in Theoretical Computer Science, vol. 126, num. 2, pp. 183-235 (1994). Rajeev Alur, Thomas A. Henzinger, Gerardo Lafferriere & George J. Pappas, "Discrete Abstractions of Hybrid Systems" in Proceedings of the IEEE, vol. 88, num. 7, pp. 971-984 (2000).
Nov 30 More model checking of concurrent software (presented by Shriram Rajagopalan). Zing project. Tony Andrews, Shaz Qadeer, Sriram K. Rajamani, Jakob Rehof & Yichen Xie, "Zing: Exploiting Program Structure for Model Checking Concurrent Software", in Proceedings of Int. Conf. on Concurrency Theory (Philippa Gardner & Nobuko Yoshida eds.), LNCS 3170, pp. 1 - 15 (2004). None.
Dec 2 Project presentations. Course project presentations None. None.
December 16 Project reports due at noon.

Links:


CPSC 513 Term 1 Winter 2009-2010 Class Page
maintained by Ian Mitchell