Formal Methods of Software Engineering
G22.3033007
Thursday, 5:007:00 PM
Room 1302, Warren Weaver Hall
Amir Pnueli and
Robert Dewar
Reaching Us
Amir Pnueli
 email
amir@cs.nyu.edu
 phone: (212) 9983225
 office: 715 Broadway, Room 707
 office hours: Wednesday 2:004:00 PM, or by appointment
Robert Dewar
 email
dewar@cs.nyu.edu
 phone: (212) 9983498
 office: WWH 511
 office hours: Wednesday 2:007:00 PM, or by appointment
Prerequisites: Some background in
algorithm design, familiarity with the language of firstorder 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 realtime 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 finitestate 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: ModelChecking 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:
SparkIntro.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