22c:181 - Formal Methods in
Software Engineering

Spring 2003

Course Syllabus

Instructor

Prof. Cesare Tinelli
201F MLH
335-0735
tinelli@cs.uiowa.edu

Office hours: Wed 2:00-3:30pm, Fri 1:30-3:00pm, or by appointment.

Teaching Assistant

Paula Kelly
101K MLH
353-2542
pkelly@cs.uiowa.edu

Office hours: Mon 2:30-3:30pm, Tue 11:30-12:30pm, Wed 12:00-1:00pm, or by appointment.

Lectures

TuTh 9:30-10:45am, 103 North Hall.

Prerequisites

Grades of C- or above in 22C:180 or 055:180, or consent of instructor.
Familiarity with basic set theory and propositional and first-order logic will be helpful.

Web Page

Most of the information about the class, including handouts and assignments, will be available from the class web site:

http://combination.cs.uiowa.edu/181

Students are expected to check both the web site and its related bulletin board on a regular basis (at least every other day) for announcements regarding the course.

Instructional Objectives

The purpose of formal methods is to enable the construction of large, highly reliable software. Their foundation is the precise specification of the run-time properties that a software system is expected to satisfy.
The case for having precise specifications is fairly obvious: without a precise specification of the software system to be built it is not possible tell that the right system is being built. Formal methods are concerned with specifications that are precise for being stated in languages endowed with a formal syntax, semantics, and theory.
Formality helps the specification process in at least two ways:
  1. it naturally leads to unambiguous, high-quality specifications, and
  2. it provides the bases for automated tool support.
As we will see in this course, formal specification techniques allow for the construction of automated verification tools that can perform tests on specifications and corresponding code to find errors in requirements, models, designs, and implementations.
In this course, we will study a collection of techniques for formal software development, spanning the whole development process: from high-level semantic modeling, to system architecture design, to coding and debugging. The study will be done not in the abstract, however, but through the use of actual tools supporting these techniques. In particular, we will study and use:

Textbook and Reading Material

There is no required textbook for this course. Reading materials will be available on the course web site. They will include several papers on formal software specification and verification, a number of papers on how to use the specification/verification tools adopted in the course, and various class notes and handouts.

Homework

Homework assignments will be related to each of the three specification/verification frameworks that we will be discussing in the course. For each of the three frameworks (Alloy, UML/USE, ESC/Java), there will be two assignments:

All assignments will be collected and graded. They are to be done individually.

Students will be also given small exercises on a fairly regular bases. Exercises are meant to help with the understanding of the course material and better prepare for the the exams. They will be neither collected nor graded.

Exams

There will be one midterm exam and one final exam. The midterm will be held during class time. The final exam will be held as per university schedule.

Grading Policy

The weighting of items in grade determination will be the following:

Class Participation 05%
Homeworks 35%
Midterm 25%
Final Exam 35%

The following cutoffs will be used to determine letter grades. In the ranges below, x stands for your total score at the end of the semester. Final scores near a cutoff will be individually considered for the next higher grade. Plus(+) and minus(-) grades will also be given; their cutoffs will be determined at the end of the semester.

Score  Grade
90 <= x < 100 A
78 <= x < 90

B

65 <= x < 78 C
55 <= x < 65 D
00 <= x < 55 F

We do not curve grades in this course. It is theoretically possible for everyone in the class to get an A (or an F). Your final grade depends only on your own performance and not on that of others

Course Policies

Assigned Readings: You are expected to do all the assigned readings.

Additional Readings and discussions: You are urged to consult sources other than our the prescribed readings, including both reserve books and additional on-line material. You are also encouraged to discuss the course topics with your classmates. It is a genuinely helpful learning activity having to formulate your own thoughts about the material well enough to express them to others.

Homework assignments: You are allowed and encouraged to discuss the homework assignments with your classmates, but you are not allowed to share solutions. Since the homework counts as a significant portion of your grade, it is expected that the submitted work be strictly your own.
(The following rule of thumb will help you not to cross the line: discuss the assignments together but do not take any written notes; go home and write the solution by yourself.)

Cheating: Copying someone else's work or sharing solutions will result in a zero on the assignment for the first offense and an F in the course for the second offense.

Late submissions: Your solutions to written assignments are to be submitted in class, before the class starts. Late written assignments can be handed in during office hours or in class. Alternatively, they can be put in the instructor's mailbox. In that case, you must notify the instructor by email at once.
Late assignments will be graded according to the following policy:

Sundays are excluded from the count of late hours.

Attendance: Students are expected to attend all classes. Your knowledge and therefore your grade depends on it. You are responsible for all announcements and material covered during class even if you did not attend. In that case, check with the instructor or with your classmates.

Extra credit: No extra-credit homeworks or tests will be given on an individual basis (although they maybe given to the whole class).

Make-up exams: Make-up exams will be offered only if there is a serious, documented reason for not being able to attend a scheduled exam, and if the request is made at least a week before the scheduled exam.

Regrading: If you think that your homework assignment has been misgraded and deserves a regrading, you are invited to let the instructor know. Regrading policies for the midterm will be announced in class when the graded exams are handed back. The instructor welcomes and will give full consideration to all well motivated regrading requests.

Special needs: The instructor must hear from anyone who has a disability that may require some modification of seating, testing, or other class requirements so that appropriate arrangements can be made. Please see the instructor after class or during office hours.

Computing Facilities

We will use the Linux workstations in the CS Educational Lab in 301 MLH. Please contact the instructor immediately if do not have a CS account yet.

Topic Outline

The outline is tentative and will be adjusted as necessary during the course of the semester.

Acknowledgments

This course is closely modeled after a similar one developed by Matthew Dwyer and John Hatcliff at Kansas State University. Much of the instructional material in this course is based on material kindly made available by them.