Formal Methods of Software Engineering
G22.3033-007
Thursday, 5:00-7:00 PM
Room 1302, Warren Weaver Hall
Amir Pnueli and
Robert Dewar
Reaching Us
Amir Pnueli
- e-mail
amir@cs.nyu.edu
- phone: (212) 998-3225
- office: 715 Broadway, Room 707
- office hours: Wednesday 2:00-4:00 PM, or by appointment
Robert Dewar
- e-mail
dewar@cs.nyu.edu
- phone: (212) 998-3498
- office: WWH 511
- office hours: Wednesday 2:00-7:00 PM, or by appointment
Prerequisites: Some background in
algorithm design, familiarity with the language of first-order logic,
and parallel programs.
Course requirements:
Assignments and a
term project.
Course Description
Software Engineering is a collection of techniques which enable
programmers and system designers to construct large software systems
in a systematic, effective, and reliable manner. They are particularly
useful for projects which involve large teams of
designers/programmers, and absolutely essential for systems which are
identified as safety critical, i.e.,
systems where a single failure may result in loss of human life.
The Formal Methods approach to software construction is based on
viewing a program and its execution as mathematical objects and
applying mathematical and logical techniques to specify and analyze
the properties and behavior of these objects. The main advantages of
the formal approach to software construction is that, whenever
applicable, it can lead to an increase of the reliability and
correctness of the resulting programs by several orders of
magnitude. Again, the main potential beneficiary of such an increase
is the class of safety critical systems.
This course consists of two mutually supportive components:
1.
State of the art approaches to Safety Critical
Systems, as illustrated by the SPARK Ada
methodology.
2.
A partial survey of formal methods for the specification and
verification of reactive and real-time systems.
Of particular importance will be the links between the two components,
where part 1 will identify the need and motivation for formal methods
and part 2 will identify the available solutions to these needs.
A partial list of the topics to be covered within part 1 is:
- Safety Critical Systems standards.
- Formal testing.
- Report of the WG9 working group on safety critical software.
- Introduction to SPARK Ada.
- A small fully worked out example.
- A survey of formal methods used in industry: Hood, Mascot, etc.
A partial list of the topics to be covered within part 2 is:
- A computational model for reactive systems.
- Specification language: Temporal Logic.
- Verification methods for sequential programs: Assertional
invariants and variants.
- Model checking of finite-state systems: explicit state and
symbolic variants.
- Deductive verification.
- Scaling up: Abstraction and (De)Composition.
Recommended Texts
- High Integrity Ada, The Spark Approach. John Barnes, Addison
Wesley.
- Systems and Software Verification: Model-Checking Techniques and
Tools. B. Berard, M. Bidoit, A. Finkel, F. Laroussinie, A. Petit,
L. Petrucci, and P. Schnoebelen, Springer.
Class Presentations
-
Lecture 0 -- Sept. 6, 2001:
Building Reliable Software.ppt,
Formal - L0.ps,
L0.pdf
-
Lecture 1 -- Sept. 20, 2001:
Formal - L1.ps,
L1.pdf
-
Lecture 2 -- Sept. 27, 2001:
Formal - L2.ps,
L2.pdf
-
Lecture 3 -- Oct. 4, 2001:
Formal - L3.ps,
L3.pdf
-
Lecture 4 -- Oct. 11, 2001:
Formal - L4.ps,
L4.pdf
-
Lecture 5 -- Oct. 25, 2001:
Formal - L5.ps,
L5.pdf
-
Introduction to Spark and Tutorial:
Spark-Intro.ppt,
Tutorial.ppt
-
Lecture 6 -- Nov. 1, 2001:
Formal - L6.ps,
L6.pdf
-
Lecture 7 -- Nov. 8, 2001:
Formal - L7.ps,
L7.pdf
-
Lecture 8 -- Nov. 15, 2001:
Formal - L8.ps,
L8.pdf
Assignments
TLV Resources