CS477/ECE478 - Formal Software Development Methods (Spring 2007)

From FSL

Students enrolled in this class are expected to check this web page regularly. Complete lecture notes will be posted here.

1 Course Description
2 Administrative Information
3 Newsgroup
4 Lecture Notes, Useful Material

Course Description

CS477/ECE478 is a course on Formal Methods and their use in software development. Formal methods is a term that refers to a diverse collection of techniques, with strong mathematical foundations, that are used to provide assurance about the correctness of systems. The course aims to familiarize students interested in software engineering with languages and methods for formal specification, development and verification. More specifically, the students will be exposed to the foundations and experimental use of the following formal methods tools:

Maude, an executable specification language with tool support for formal analysis, including theorem proving and model checking;
Java PathFinder and JavaFAN, two model checkers for Java; and
JavaMOP, a runtime verification framework for Java

Administrative Information

Meetings: Tu/Th 9:30 - 10:45, 1103 Siebel Center

Credit: 3 or 4 credits

Professor: Grigore Rosu (Office: SC 2110)

Office hours: 10:00 - 12:00 on Mondays (held by Grigore Rosu in SC 2110)

Web site: https://fsl.cs.uiuc.edu/index.php/CS477/ECE478_-_Formal_Software_Development_Methods_%28Spring_2007%29

Newsgroup

news://news.cs.uiuc.edu/class.cs477

Lecture Notes, Useful Material

The links below provide you with useful material for this class, including complete lecture notes. These materials will be added by need.

Introduction (updated on January 17, 2007; complete) [L1]
Maude (updated on January 18, 2007; complete) [L2,L3]

2 HW1 exercises (see pages 24 and 55), due Tuesday, February 6
Maude modules mentioned in the lecture notes

Formal Definition of a Simple Programming Language (updated on January 25, 2007; complete) [L4]

1 HW1 exercise (see pages 29-30), due Tuesday, February 6
Maude modules mentioned in the lecture notes

Inductive Theorem Proving (updated on January 30, 2007; complete) [L5,L6,L7,L8]

4 HW2 exercise, due Tuesday, February 27: Homework description and source files .
ITP downloading

Maude and ITP modules

(linux version)

Maude and ITP modules

(windows version). If this doesn't work, you may try

the emulated version

, or try to build it yourself on your machine - just be sure to build the 2.1.1 version.

only the ITP

The ITP user manual

ITP installation and use instructions

Download the zip file, unzip-it, run ./maude, (or, for windows natve, maude.exe, or, for windows emulated, maude.bat)

load your module e.g., in natural.maude,

load the ITP: in itp-tool. Initialize it: loop init-itp . and you're in :)

provided proof scripts have the extension .itp

Verification of Sequential Programs (updated on February 13, 2007) [L9,...]

Lecture slides on discovering loop invariants

(uploaded on March 26, 2007)

2 HW3 exercises, due Sunday, March 18: Homework description and source files .
On Java+Itp page you can find

The latest version of the tool (still, for the homewortk you should use the one provided in the archive)
Documentation: a technical report describing in depth both the definition of Java and the tool commands (with examples)

1 Extra Credit exercise, due Monday, March 26: Description .

Verification of Concurrent Programs (updated on March 24, 2007; complete)

Maude sources extracted from the slides
3 HW4 exercises, due Tuesday, April 17: Homework description .

Unit Project Description (updated on April 15, 2007)
JavaFAN (updated on May 1, 2007)

2 HW5 exercises, due by end of term: Homework description and working code (updated on April 30, 2007)
Readers/writers java definition and property spec: rw.zip