CSci 420/520: Software Development with Formal Methods

Syllabus

Where and When

• Class: 1:00-1:50 MWF, Small Physics Lab, Room 240.
• Professor office hours: 2:00-4:00 MW, and by appointment. 140 McGloughlin-Street Hall.
• TA (Meghan Revelle meghan@cs.wm.edu) office hours: 10-11 TT. 101-c McGloughlin-Street Hall.

Instructor

David Coppit (http://www.cs.wm.edu/~coppit/, coppit@cs.wm.edu). Research: software plans, software development methods, applied formal methods, software verification.

Web Page

Course homepage: http://www.cs.wm.edu/~coppit/csci420-fall2005/. Contains the definitive versions of assignments and such.

Description

From the catalog: "This course covers the use of formal specification techniques and tools for the rigorous development of trustworthy software."

Society is increasingly reliant on software, and yet our ability to produce trustworthy software is woefully inadequate. At least part of the blame lies with our techniques for educating software developers, which focus on the mechanics of programming rather than the process of engineering software. Indeed, software engineering, unlike other engineering disciplines, is still a part of its associated science—computer science—rather than a separate discipline. As a result, little time remains in most curricula to teach rigorous engineering techniques for the development of trustworthy software.

This course attempts to address this problem at the College of William and Mary. Using state-of-the-art languages and tools, students will practice thinking rigorously about software, developing and validating formal models of the software, implementing those models, then verifying the correctness of those implementations.

This course will emphasize writing and validation of specifications rather than implementation, since this is what students are least familiar with. We will use different tools for different formal methods: PVS for theorem proving of specification, Alloy Analyzer for model checking specifications, and ESC/Java and Java PathFinder for verifying implementations.

Students who complete this course successfully will know how to:

• Write a formal specification of the key elements of a software system, in both the PVS and Alloy languages
• Use the PVS theorem prover to prove properties of a specification
• Use the Alloy Analyzer model checker to check properties of a specification
• Implement a specification, and use design-by-contract to embed checks in the software

It is assumed that students already have programming experience. This course will not devote much time to coding, debugging, or other basic software knowledge which the student should have acquired earlier in the curriculum.

CSci 520

This course is cross-listed as CSci 520. Graduate students are expected to perform more work than undergraduates, including but not limited to a course project.

Project

CSci 535 students will complete a project where they apply the techniques learned in the course. The project is expected to include a significant formal specification and validation component. Optionally, students may also implement the software that they specify, using program verification tools. Examples of projects include software for an ATM, cruise control, network protocol, or a cell phone contacts database.

Each student is expected to discuss his or her project ideas with the professor prior to writing and submitting a formal proposal. Students will also be required to submit a progress report and a final report. At the end of the semester, students will present their projects to the class.

Prerequisites

CSci 243 and CSci 301

Some Topics

• Formal specification
• Theorem proving
• Model checking
• Program verification
• Cleanroom software development

Books

There are none. Instead, students will read papers.

Grading

CSci 435 Point Distribution

• Midterm exam: 15%
• Final Exam: 25%
• Homework: 50%. The homework assignments will be subject to a weighted average.
• Class Participation: 10%. This subjective grade is given by the professor based on the student's in-class discussion of papers, lecture questions, etc.

Class participation works principally like this: at the start of the semester, a random ordering of students in the class will be created, duplicating some student names as necessary. On any given day, the next person in the list will be asked to summarize and start the discussion of the paper. This person will lose participation points if he or she cannot do a good job introducing the paper.

CSci 535 Point Distribution

• Midterm exam: 15%
• Final Exam: 25%
• Project: 25%. There will be several project milestones, and your grades for the milestones may be subject to a weighted average.
• Homework: 35%. The homework assignments will be subject to a weighted average.

The "No BS" Rule

The student gets 10% on short-answer questions in which the answer given is "No BS". Note: not turning in a test or exam gets you a 0.

Letter Grade

• 90% ≤ grade < +∞ → A
• 80% ≤ grade < 90% → B
• 70% ≤ grade < 80% → C
• etc. ... but the professor makes the final call on all grades.

Late Work Policy

20% of the points are lost per day (or portion thereof) that an assignment is late. Example: Due Monday at 5pm, and you turn it in 6pm Tuesday: -40%

Make-up Policy

Tests can be made up with prior approval of the instructor. Your final exam schedule can only be altered by the Office of Student Affairs.

Students Who Need Accommodation

Please see me after class or send email to set up a brief meeting.

Guidelines for Class Assignments

• The Honor Code is always in effect, unless the professor says otherwise
• External material: feel free to use the internet, books, etc. If you happen to find a solution to a problem, do yourself a favor and avoid it.
• Fellow students: Help each other with general questions, but don't give away the strategy or "secret" of a problem. Let the professor give hints if necessary on the website.