ICS 222: Formal Methods in Software Engineering

ICS 222: Formal Methods in Software Engineering

Debra J. Richardson and David S. Rosenblum

Course Description
Catalog Copy

Examination of formal specification models, including algebraic/axiomatic, state-transition, model-based, operational, and temporal logics, along with their related analysis techniques. Formal models in software development are discussed as are different proof techniques.

This course will examine formal specification and analysis methods and their use in Software Engineering. A secondary focus of the class will be on the many software development activities that benefit from the use of formal methods. Students will study different types of formal specification languages and utilize specific languages to describe software systems. In addition, various tools are available for use that support the discussed formal specification languages and facilitate software development activities, including but not limited to proving program correctness.

At the end of the course students should be conversant with the primary current approaches to formal methods and their use in software engineering. Students should be familiar with the "canonical" examples typically used in research papers. Students should also be aware of the major open problems in the use of formal methods in software engineering, such that research within this domain would be a natural follow-on to this course.

Course requirements are reading relevant papers on formal methods, participation in class, satisfactory performance on pop quizzes covering the reading material, and a quarter project, which includes three short presentations. There are several options (discussed below) for the quarter project, the primary requirement being that it focus on some formal method.

Prerequisites

ICS 221 is recommended but not required.

Schedule and Assigned Readings

(subject to change; additional readings may be assigned)

Date	Topic	Readings	Lecturer
April 6	Course Overview		Richardson & Rosenblum
April 8	Introduction to Formal Methods	[Win90] [Hal90] [Kem90]	Richardson
April 13	Formal Specification Languages	[Har87] [Mey85] [Flo67]	Richardson
April 15	Axiomatic Specification	[Hoa69] [LvH85]	Rosenblum (DJR absent)
April 20	Algebraic Specification	[GT79] [GHW85]	Rosenblum
April 22	Temporal Logic Specification	[Lam83] [Dil92]	Richardson
April 27	EDCS		(DSR & DJR absent)
April 29	Project Briefs		all students
May 4	Formal Verification	[HK76] [ILL75] [DLP79]	Rosenblum
May 6	Category Theory	[WE98]
May 11	Formal Architecture Description	[AG97]	Richardson (DSR absent)
May 13	Student Topic Presentations		1,2
May 18	ICSE '99 *		(DSR & DJR absent)
May 20	ICSE '99 *		(DSR & DJR absent)
May 25	Student Topics		3,4.5
May 27	Student Topics		6,7
June 1	Student Topics		8,9,10
June 3	Student Topics		11,12
June 8	Final Project Presentations		five students
June 10	Final Project Presentations		five students
June 17	Final Project Presentations (final exam period, if needed)		five students

* Students strongly encouraged to attend ICSE in Los Angeles, May 19-21

Readings

[AG97] R. Allen and D. Garlan. "A Formal Basis for Architectural Connection", ACM Transactions on Software Engineering and Methodology, 6(3):213-249, July 1997.

[DLP79] R.A. DeMillo, R.J. Lipton and A.J. Perlis. "Social Processes and Proofs of Theorems and Programs", Communications of the ACM, 22(5):271-280, May 1979.

[Dil92] L.A. Dillon, G. Kutty, L.E. Moser and P.M. Melliar-Smith. "Graphical Specifications for Concurrent Software Systems". Proc. of the 14th Int’l Conf. On Software Engineering (ICSE-14), May, 1992, pp. 214-224.

[Flo67] R.W. Floyd. "Assigning Meanings to Programs", Proc. of a Symposium on Applied Mathematics vol. XIX, American Mathematical Society, May 1967..

[GHW85] J.V. Guttag, J.J. Horning, and J.M. Wing. "The LARCH Family of Specification Languages," IEEE Software ; 2(5):24-36,September 1985.

[GT79] J.A. Goguen and J.J. Tardo. "An Introduction to OBJ: A Language for Writing and Testing Algebraic Program Specifications," Specifications of Reliable Software, 1979.

[Hal90] A. Hall. "Seven Myths of Formal Methods," IEEE Software; 7(5), September 1990.

[HK76] S.L. Hantler and J.C. King. "An Introduction to Proving the Correctness of Programs," ACM Computing Surveys, September 1976.

[Har87] D. Harel. "Statecharts: A Visual Formalism for Complex Systems," Science of Computer Programming, 1987.

[Hoa69] C.A.R. Hoare. "An Axiomatic Basis for Computer Programming", Communications of the ACM, 12(10), October 1969.

[ILL75] S. Igarashi, R.L. London, and D.C. Luckham. "Automatic Program Verification I: A Logical Basis and Its Implementation," Acta Informatica, 4:145-182, 1975.

[Kem90] R.A. Kemmerer. "Integrating Formal Methods into the Development Process", IEEE Software, 7(5):37-50, September 1990.

[Lam83] L Lamport. "What good is temporal logic?" Information Processing, 1983.

[LvH85] D.C. Luckham and F.W. von Henke. "An Overview of Anna, A Specification Language for Ada", IEEE Software, 2(2):9-23; March 1985.

[Mey85] B. Meyer. "On Formalism in Specifications", IEEE Software, 2(1):6-26, January 1985.

[Par93] D.L. Parnas. "Predicate Logic for Software Engineering", IEEE Transactions on Software Engineering, 19(9):856-862, September 1993.

[WE98] V. Wiels and S. Easterbrook. "Management of Evolving Specifications Using Category Theory", Proc. 13th IEEE Int’l Conf. on Automated Software Engineering, October 1998.

[Win90] J.M. Wing. "A Specifier's Introduction to Formal Methods", IEEE Computer, 23(9):8-24, September 1990.

Suggested topics for student presentations

Logic and Critical Reasoning

Logics and Proof Systems
Denotational Semantics
Category Theory

Formal Specification Languages

Axiomatic Specifications
Algebraic Specifications
State-Transition Specifications
Abstract Model Specifications
Concurrency Specifications
Temporal Logic Specifications
Operational Specifications
Multi-Paradigm Specifications
Process Algebras

Applications for Formal Methods

Verification by Automated Theorem Provers
Model Checking
Simulation
Testing
Architecture Description and Analysis
Reuse
Change Management
Hardware/Software Co-Design
Protocol Specification and Verification
Formalized Development Processes (e.g. Cleanroom)

Assessment

5% Class Participation

10% Pop Quizzes

5% Project Brief (5 minutes)

50% Term Project, chosen from

UML Formalization
Formal Methods capability for TIDE
Formal Specification of Free Flight Application
other topics to be proposed by instructors
topic chosen by student and approved by instructor

Graded on effort and on final report turned in at end of class

Three options:

Combined 222+224 project, done individually
224-only project, done individually
224-only project, done with at most one other person

Options (A) and (C) would naturally involve projects that are larger in scope than those for (B).

Each option requires each student to do a half-period lecture (see next)

20% Presentation of a Topic in analysis and testing relevant to chosen project (30 minutes),

including presentation of background readings and description of project application of topic

10% Final presentation of project (15 minutes)

NOTE: There will be no incompletes (I grades) granted, except in truly rare and unavoidable circumstances. All course work must be completed by the end of finals week.