Schedule
The following table shows a tentative schedule of the course. The schedule is subject to change, as topics will be decided upon during the first few course meeting. If changes are necessary, this page will be updated.
| Weeks | Dates | Topics | Readings | Assignments |
|---|---|---|---|---|
| Week 1 | Jan. 19 | Introduction | Chapter 1 | |
| Jan. 21 | Cleanroom Methods | |||
| Week 2 | Jan. 26 | States and Functions | Sections 2.1-2.4 | |
| Jan. 28 | Intended Functions | Sections 2.5-2.7 | ||
| Week 3 | Feb. 2 | Verification | Sections 3.1-3.5 | |
| Feb. 4 | Trace Tables | Sections 3.5-3.7 | Homework 1 | |
| Week 4 | Feb. 9 | Verification of Iterations | Sections 4.1-4.2 | |
| Feb. 11 | Verification of Iterations | Sections 4.3-4.5 | ||
| Week 5 | Feb. 16 | Programming with Intended Functions | Sections 5.1-5.3 | |
| Feb. 18 | Group Work | Sections 5.4-5.5 | Homework 2 | |
| Week 6 | Feb. 23 | Verification Review | Sections 6.1-6.3 | |
| Feb. 25 | ||||
| Week 7 | Mar. 2 | Definite Iteration | Sections 7.1-7.3 | |
| Mar. 4 | Definite Iteration | Sections 7.4-7.7 | ||
| Week 8 | Mar. 9 | Data Abstraction | Sections 8.1-8.3 | |
| Mar. 11 | Object-Oriented Programs | Sections 8.4 | Hoemwork 3 | |
| Week 9 | Mar. 15-19 | Spring break | ||
| Week 10 | Mar. 23 | Recursion | Sections 9.1-9.3 | |
| Mar. 25 | Introduction to Formal Methods (Cesar Yeep, 4/06) | [Wing90]
[Saiedian96] |
||
| Week 11 | Mar. 30 | |||
| Apr. 1 | Proposal Presentation | Project proposal | ||
| Week 12 | Apr. 6 | Formal BISL: JML (Cyrus Brooks, 4/08) | [Leavens-Baker-Ruby06]
[Leavens-Baker-Ruby99] [Burdy-etal05] |
|
| Apr. 8 | JML | |||
| Week 13 | Apr. 13 | Tabular Notation (Melisa Vela, 4/20) |
[Janicki-Parnas-Zucker96]
[Parnas92] [Parnas93] |
|
| Apr. 15 | OCL (Carmen Avila, 4/22) | Handout | ||
| Week 14 | Apr. 20 | Formal Specification Language: Z (Rafa Escalante, 4/22) | [Spivey89]
[Woodcock89] |
|
| Apr. 22 | VDM-SL (Christian Del Hoyo, 4/27) | [Hayes-Jones-Nicholls94]
[Bicarregui-Ritchie95] [Duce-Fielding87] |
||
| Week 15 | Apr. 27 | Process Algebra: CCS and CSP (Bhanukiran Gurijala, 4/27) | [Hoare78]
[Brinksma86] |
|
| Apr. 29 | CCS and CSP | |||
| Week 16 | May 4 | Project Presentation | Project Report | |
| May 6 | Project Presentation |
Readings
The following is a list of tentative readings. The list is subject to change, and you will be asked to add your own reading list; an up-to-date list will be available from the course Web page. To download the PDF files, use the login-name and password that will be announced in class.
- [Bicarregui-Ritchie95]
Juan Bicarregui and Brian Ritchie.
Invariants, Frames and Postconditions: a Comparison
of the VDM and B Notations
IEEE Transactions on Software Engineering, 21(2):79-89, February 1995.
[PDF]
- [Brinksma86]
Ed Brinksma.
A Tutorial on LOTOS.
In Protocol Specification, Testing, and Verification,
V, pages 171-194, Elsevier, 1986.
[PDF]
- [Burdy-etal05]
Lilian Burdy, Yoonsik Cheon, David Cok, Michael Ernst, Joe Kiniry,
Gary T. Leavens, K. Rustan M. Leino, and Erik Poll.
An Overview of JML Tools and Applications,
International Journal on Software Tools for Technology Transfer,
7(3):212-232, June 2005.
[PDF]
- [Duce-Fielding87]
D. A. Duce and E. V. Fielding.
Formal Specification --- A Comparison of Two Techniques.
The Computer Journal, 30(4):316-327, 1987.
[PDF]
- [Hall90]
Anthony Hall.
Seven Myths of Formal Methods.
IEEE Software, 7(5):11-19, September 1990.
[PDF]
- [Hayes-Jones-Nicholls94]
I.J. Hayes, C.B. Jones and J.E. Nicholls.
Understanding the Differences Between VDM and Z.
Software Engineering Notes, 19(3):69-74, July 1994.
[PDF]
- [Hoare69]
C.A.R. Hoare.
An Axiomatic Basis for Computer Programming.
CACM, 12(10):576-583, October 1969.
[PDF]
- [Hoare72]
C.A.R. Hoare.
Proof of Correctness of Data Representation.
Acta Informatica, 1:271-281, 1972.
[PDF]
- [Hoare78]
C.A.R. Hoare.
Communicating Sequential Processes.
Communications of the ACM, 21(8):666-677, August 1978.
[PDF]
- [Janicki-Parnas-Zucker96]
Ryszard Janicki, David L. Parnas, and Jeffery Zucker.
Tabular Representations in Relational Documents.
In Relational Methods in Computer Science,
Springer-Verlag, 1996.
[PDF]
- [Leavens-Baker-Ruby99]
Gary T. Leavens, Albert L. Baker, and Clyde Ruby.
Preliminary Design of JML: A Behavioral Interface Specification
Language for Java,
ACM SIGSOFT Software Engineering Notes,
31(3):1-38, March 2006.
[PDF]
- [Leavens-Baker-Ruby99]
Gary T. Leavens, Albert L. Baker, and Clyde Ruby.
JML: A Notation for Detailed Desing,
In Behavioral Specifications of Businesses and Systems,
chapter 12, pages 175-188, Kluwer, 1999.
[PDF]
- [Linger94]
Richard C. Linger.
Cleanroom Process Model.
IEEE Software, 11(2):50-58, March 1994.
[PDF]
- [Parnas92]
David L. Parnas.
Tabular Representation of Relations.
CRL Report 260, Communication Research Laboratory,
McMaster University, October 1992.
[PDF]
- [Parnas93]
David L. Parnas.
Predicate Logic for Software Engineering.
IEEE Transactions on Software Engineering,
19(9):856-862, September 1993.
[PDF]
- [Saiedian96]
Hossein Saiedian (ed).
An Invitation to Formal Methods.
IEEE Computer, 29(4):16-30, April 1996.
[PDF]
- [Spivey89]
J.M. Spivey.
An Introduction to Z and Formal Specifications.
Software Engineering Journal, 4(1):40-50, January, 1989.
[PDF]
- [Stavely95]
Allan M. Stavely.
Verifying Definite Iteration Over Data Structures.
IEEE TSE, 21(6):506-514, June 1995.
[PDF]
- [Wing90]
Jeannette M. Wing.
A Specifier's Introduction to Formal Methods.
IEEE Computer, 23(9):8-24, September, 1990.
[PDF]
- [Woodcock89]
J.C.P. Woodcock.
Structuring Specifications in Z.
Software Engineering Journal, 4(1):51-66, January, 1989.
[PDF]
Last modified by Yoonsik Cheon: $Id: schedule.html,v 1.33 2010/04/21 23:02:12 cheon Exp $