Tutorial on Formal Methods

Dr. Ann E. Kelley Sobel

sobelae@muohio.edu

Associate Professor, Miami University, Oxford, OH

Wednesday, May 27 - Friday, May 29, 1998

Room 152, NIST North, Gaithersburg, MD

High quality computer systems can no longer be developed with just the specify/build/test paradigm. Formal methods are an important adjunct to reduce ambiguity and inconsistency, verify complex algorithms, and increase automation. We are fortunate to have Dr. Ann Sobel visiting NIST to teach a three-day tutorial on formal methods in software development. Obviously there is not time to teach all of formal methods in a few days, but this tutorial is designed to give the attendees some useful skills and ideas about how to continue.

Dr. Sobel has developed and teaches a 4-year Bachelor degree program in software engineering based on Formal Methods. Students in the course learn programming languages just as well as those in a traditional program, but naturally approach problems from a requirements-first (rather than code-then-debug-to-taste) perspective.

Schedule

Date	Session	Time	Subject
Wed, May 27	I	9:00 - 10:20	Introduction to Formal Methods
	IIa	10:40 - 12:00	First Order Logic
	IIb	1:00 - 2:20	Formal Specification and Program Derivation
	IIc	2:40 - 4:00	Program Derivation
Thu, May 28	IIIa	9:00 - 10:20	An Operational Specification Model
	IIIb	10:40 - 12:00	An Operational Specification Model
	IVa	1:00 - 2:20	A Software Engineering Curriculum Centered on FM
	IVb	2:40 - 4:00	Results of A Software Engineering Curriculum Centered on FM
Fri, May 29	Va	9:00 - 10:20	Z: a Model-Based Formalization
	Vb	10:40 - 12:00	Z: a Model-Based Formalization
	VI	1:00 - 2:40	CSP: a Message-Based Formalization

Registration

There is no cost for the tutorial. This is open to the public. Participants need not attend every session. To register, send e-mail to Paul Black (paul.black@nist.gov) or call him at 301-975-4794.

Currently there is no plan to present the tutorial again. However if there is interest, we will consider it. Copies of the slides are available free of charge from Dr. Black.

Prerequisites

Texts

A Logical Approach to Discrete Mathematics
Gries and Schneider

Programming in the 1990's: An Introduction to the Calculation of Programs
E. Cohen

An Introduction to Formal Specification and Z
Potter, Sinclair, & Till

Communicating Sequential Processes
Communications of the ACM, Vol. 21, No. 8, 1978, pages 666-677
C.A.R. Hoare

The use of formal logic in solving problems can be demonstrated with logic puzzles such as those in books by Raymond M. Smullyan: First-Order Logic, What Is the Name of This Book? : The Riddle of Dracula and Other Logical Puzzles, Forever Undecided : A Puzzle Guide to Godel, etc.

Session Details

What are formal methods? How can I use them? Overview of different formal methods, modeling languages, applicable domains, etc.

Students learn a formal logic, how to formally specify software, and how to derive programs from these specifications.

Students learn the Operational Specification Model used in the Software Engineering course.

What and how are formal methods taught in a software engineering curriculum? What are the results? What are the costs in terms of staff and support? This session will use examples in the model explained in Sessions II and III.

Z (pronounced "zed") is a widely used model-based formalization. This session teaches Z and gives some examples of its use.

CSP (Communicating Sequential Processes) is another formalization particularly good at modeling distributed systems and parallel computations.