Reactive software systems are becoming an integral part of nearly every engineered product: they control consumer products, commercial aircraft, nuclear power plants, medical devices, weapon systems, aerospace systems, automobiles, public transportation systems, and so on. At the same time quality and confidence issues are increasing in importance. Errors may result in loss of life, destruction of property, failure of businesses, and environmental harm. Today, designers check that a reactive software system works properly by using simulation and testing. However, as reactive systems become more complex and pervasive, these traditional techniques are not sufficient to assure desired reliability. Abstract interpretation, model checking and related computer-aided verification techniques are emerging as practical alternatives. They allow the designer to verify that a software system satisfies its abstract logical specification. This approach has been most effective for control-intensive components, and is rapidly becoming an integral part of the design cycle in many embedded software companies.
The participants will learn how to model a reactive (hardware or software) sytem, express desired properties of the reactive system and check that the system satisfies these properties. They will get familiar with the algorithmic methods used for this check.
The course requires basic knowledge of algorithms, data structures, automata theory, computational complexity, and propositional logic. Knowledge of operating systems, communication protocols, and hardware is useful. The course requires mathematical maturity, and is appropriate for graduate students who wish to pursue research in formal methods or related areas. If you need more information to decide, contact the instructor.
The course introduces the operational semantics of
reactive
software systems as a fundamental instrument in developoing tools and
techniques for the automated verification of temporal (logic)
properties
of software systems.
The emphasis is on the underlying logical and automata-theoretic
concepts, the
algorithmic solutions, and heuristics to cope with the high
computational
complexity. Topics include
We will look at various tools including:
The course will use a selection of papers considered to be among the most relevant in this area.
There will be no exams.
There will be periodic homework assignments and a class project. The project can be done in groups of two or three, and will require a presentation in the final week. Projects can be of various forms:
|
|
||||
|
|
Date |
Topic |
Paper |
Slides |
|
1. |
Aug 31 |
- Computer
aided software analysis: Overview, requirements specification,
reactive programs, compilation process, program abstraction, data-flow
and control-flow graphs, program analysis, and software model checking. |
|
|
|
2. |
Sep 02-14 |
- Abstract
Interpretation: Syntax and Semantics of programs, static
semantics, consistent abstract interpretation, lattice of abstract
interpretations, abstract evaluation of programs, Fixpoint
approximation methods, widening and narrowing. |
||
|
*** |
Sep 16 |
Rosh Hashanah (no class) |
|
|
|
3. |
Sep 21-30 |
- Predicate
Abstraction: parallel systems, predicate transformers, abstract
semantics of programs, abstract state lattice, abstract transitions,
computing abstract successors abstract state space exploration,
complexity, abstract state graph construction, state graph refinement
implementation, reachability algorithm, applications |
||
|
4. |
Oct 3-12 |
- Abstraction refinement: Overview
of the SLAM toolkit, the predicate abstraction tool C2bp, the model
checking tool for boolean programs Bebop and the automatic refinement
tool Newton. |
||
|
5. |
Oct 14-21 |
-
Automated predicate abstraction of C Programs: Challenges of
predicate abstraction in C, weakest precondition and cubes, pointers
and aliasing, predicate abstraction for assignments, gotos and
conditionals, and procedure calls, soundness and completeness, the C2bp
tool. |
||
|
6. |
Oct 23-30 |
- Model
checking boolean programs: Hierarchic state machines, push-down
automata and boolean programs, statements, variables and scope,
construction of the control flow graph, trace semantics, reachability
via interprocedural dataflow analysis, path edges, summary edges,
transfer functions, shortest trajectories, optimizations, the Bebop
tool. |
|
|
|
18. |
Nov 04-25 |
- Counterexample driven refinement: Explaining infeasible paths, path simulation via strongest postconditions, abstract explanations, basic path simulation, procedures and pointers, implementation in the {\sc Newton} tool, experiments. |
|
|
|
*** |
Nov 27 |
Thanksgiving (no class) |
|
|
|
25. |
Dec 02-16 |
- Transition predicate abstraction: Automata-theoretic verification of concurrent programs, liveness and fair termination, abstract transition programs, transition predicates, automated abstraction, just termination, compassionate termination, lexicographic completeness. |
|
|
Last updated on Dec 16, 2004 by Radu
Grosu