CSE814 Formal Methods in Software Development 
Syllabus for Fall 2009

Instructor:

Dr. Laura Dillon, 3132 Engineering Building. (ldillon@cse.msu.edu)

Office Hours: M: noon-1:30 pm, TH: 3:00-4:20 pm, and by appt.

Phone: (517)-355-4387

Class:

MW, 3:00-4:20 pm, 305 Bessey

Recommended* Textbooks:

High Integrity Software, The SPARK Approach to Safety and Security
John Barnes.  Addison-Wesley, 2006

Software Abstractions: Logic, Language, and Analysis
Daniel Jackson. MIT Press 2006

 

Concurrency: State Models and Java Programs
Second Edition
J. Magee and J. Kramer. John Wiley & Sons publishers, 2006

*We will discuss some form of book sharing so students do not need to purchase all of these books.

Course Abstract:

Formal methods are used to precisely specify and reason about various aspects of software systems. They find a variety of uses at different stages in the software lifecycle, e.g., during conceptual analysis and specification, design, and verification. At the end of this course, you should be able to:

• understand and use design-by-contract for documentation and for proving a program is correct 
• create analytical models of software designs and use simulation/model-checking techniques to analyze these models
• use formal notations and proof to specify and refine software requirements
• exploit formalism to help organize and write specification documents, even if the resulting documents contain no formalism

In addition, you will gain an appreciation for the complexity of design and verification of software systems and the ways in which formal methods can be applied to ameliorate this complexity.

Topics to be covered include:

• Design-by-contract (DBC)
• Information flow analysis
• Proof of correctness
• Analytical models of software designs
• Fundamentals of software specification; specifically, how to be abstract without being imprecise.
• Specification paradigms:
  • Contracts (e.g., SPARK Ada)
  • Model-based techniques (e.g., Alloy)
  • Action languages and notations for reasoning about concurrency (e.g., FSP)
  • (time permitting) Temporal logics (e.g., PTL and GIL)
• Formal refinement.
• Automated analysis of behavioral specifications

Requirements:

Students should be familiar with logic and the fundamentals of software engineering, including the use of informal modeling notations, such as UML class diagrams. Students should have experience in the development of a software system of reasonable size. Students should be familiar with the fundamentals of programming languages, formal-language theory (including parsing), algorithms and data structures, and discrete mathematical structures.

Grading:

Your grade will be determined as follows. 50% will come from homework assignments, which I will issue every week or two and which you must complete without consultation with other students. The other 50% will come from a term project based on a write-up (30%) and presentation (20%). 

There will be no in-class exams of any kind; nor will there be a final exam as such. However, we will meet during the final exam period (Monday December 14, 3:00-5:00 pm) for the project presentations, and your attendance is required at this final meeting. The project may be done with a partner or individually. With any written document, a good part of the grade will be based on clarity, good organization, and correct use of English. All grades become final five days after I return the graded papers. Any assignment that is not turned in by the due date will receive a grade of 0.

Integrity and ethics:

The policy of the university on integrity of scholarship and grades will be followed. Implicit in handing in homework and exams is that they represent the student's own work. Any exceptions should receive prior approval from me and must be explicitly noted in the submitted work. Representing someone else's work as one's own is grounds for failing the course.