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

From FSL
Jump to: navigation, search

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


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



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.

  • 25px-Pdf_icon.png Introduction Info_circle.png (updated on January 17, 2007; complete) [L1]
  • 25px-Pdf_icon.png Maude Info_circle.png (updated on January 18, 2007; complete) [L2,L3]
  • 2 HW1 exercises (see pages 24 and 55), due Tuesday, February 6
  • 25px-Zip_icon.png Maude modules Info_circle.png mentioned in the lecture notes
  • 1 HW1 exercise (see pages 29-30), due Tuesday, February 6
  • 25px-Zip_icon.png Maude modules Info_circle.png mentioned in the lecture notes
25px-Zip_icon.png Maude and ITP modules Info_circle.png (linux version)
25px-Zip_icon.png Maude and ITP modules Info_circle.png (windows version). If this doesn't work, you may try 25px-Zip_icon.png the emulated version Info_circle.png, or try to build it yourself on your machine - just be sure to build the 2.1.1 version.
25px-Zip_icon.png only the ITP Info_circle.png
25px-Pdf_icon.png The ITP user manual Info_circle.png.
  • 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
25px-Pdf_icon.png Lecture slides on discovering loop invariants Info_circle.png (uploaded on March 26, 2007)
  • 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:25px-Pdf_icon.png Description Info_circle.png.
Personal tools