Course goal

Both a paper and a project will be required.

• Paper: Discuss some formal method. (Preferably one we haven't discussed in class.) Who first developed the concept? Describe it and discuss how it is supposed to help improve the software development process. (That is the easy part.) Then do a literature search and discuss how well the claims of the proponents of the technology have been validated. What validation has been done on the technology and how effective has it been?
• Project: You are to evaluate an implemented tool and write a report on your assessment of its effectiveness.
  1. Choose some tool. The following tools are now available on aaron: pvs (in /aaron/pvs), alloy (in /aaron/alloy), spin (in /aaron/spin), and nqthm (Boyer-Moore theorem prover) (in /aaron/boyer-moore). You may use some other tool, but you have to download it yourself and ask for permission to evaluate it.
  2. Set your path to access directory. Usually setenv PATH /aaron/filename:{$PATH}
  3. Use tool to develop and verify some non-trivial program or specification. This should be one of your own and not a finished example you found on the internet.
  4. Evaluate the effectiveness, ease of use, execution speed and any other characteristic of the program you think important.
  5. Turn in (it can be via email): the source file verified, the output of the verifier, and your written evaluation.
• Class report: Each student will have to report on one of the above two activities during the last week of the semester.

• September 17 - Sample axiomatic problems

No textbook is required. Various readings will be distributed in class or available through this web page. For references from easily accessible journals (e.g., Communications of the ACM, IEEE Software, IEEE Computer, IEEE Transactions on Software Engineering) you are expected to obtain your own copy.

Date	Topics	References
		Basic text for first few weeks = Gannon, Purtilo, Zelkowitz 1994 text on formal methods
September 2-4	Validation of new software engineering methods; Software engineering technology transfer Slides	"Experimental validation in software engineering" by Marvin V. Zelkowitz and Dolores Wallace" Information and Software Technology (November, 1997) 734-744 (pdf). "Software Engineering technology infusion within NASA," by M. V. Zelkowitz, IEEE Trans. on Eng. Mgmt. 43, 3 (August, 1996) 250-261 (pdf). A. Hall. Seven Myths of Formal Methods. IEEE Software, 7(5):11-19, September 1990
September 9-11	Classical formal methods: Axiomatic verification, weakest precondition	"The role of verification in the software specification process," by M. Zelkowitz, Advances in Computers 36, Academic Press (1993) 43-109 (pdf). C. A. R. Hoare, "An Axiomatic Basic for Computer Programming," Communications of the ACM, Vol. 12, No. 10, 1969, pp. 576-580, 583. (This is the seminal paper on this topic) Notes on axiomatic proofs (pdf) Slides on predicate transforms (pdf)
September 16-18	Algebraic data types	Notes on algrebraic data types (pdf)
September 23	Functional verification	See Advances in Computers article
September 25	Denotational semantics	See Advances in Computers article
September 30-October 2	No Class this week
October 7-9	Z	Z Manual by J. M. Spivey
October 14-16	PVS	PVS Tutorial; PVS User Guide FAQ about Larch Larch Technical Report Larch/C++ report
October 21-October 23	Cleanroom, Case studies	"Cleanroom Software Engineering" by H. D. Mills, M. Dyer, and R. C. Linger, IEEE Software (September, 1987) 19-25. Case studies: Ariane 5, Therac 25, NASA MPO and MCL Ariane 5 failure Quicktime video of Ariane 5
October 28	Midterm review
October 30	Midterm
November 4	Boyer Moore Theorem prover	Introduction to BM Overview paper
November 6	No class	Candidate for cancelling
November 11	Temporal logic	Pages 223-230, 1994 text
November 13	Model checking	NASA SPIN example SPIN paper Alloy - Dan Jackson Alloy Manual
November 18	Lightweight formal methods	M. Heimdahl and N. E. Leveson, Completeness and consistency in hierarchical state-based requirements, Transactions on Software Engineering, (22)6, June, 1996, 363-377. E. Clarke, J. M. Wing, Formal methods: State of the art and future directions S. Easterbrook, R.R. Lutz, R. Covington, J.C. Kelly, Y. Ampo, and D. Hamilton. Experiences Using Lightweight Formal Methods for Requirements Modeling. IEEE Transaction on Software Engineering, January 1998.
November 20	Automatically generated test cases
November 25	No class	Candidate for cancelling
November 27	No class	Thanksgiving Holiday
December 2	Practical Formal Methods Research
December 4	Class reports
December 9	Final Exam
December 11	No class	Candidate for cancelling