Reading reviews

Students must hand in a short review of every paper that is assigned. To help us take the best advantage of our short time together in lecture, reading a lecture's papers and doing the reviews must be completed before the lecture. Each review consists of the following parts:

• A one-paragraph summary of the paper, plus answers to the following questions:
• To which general class(es) of software is the technology best suited? e.g. consumer products, desktop applications, mission- or safety-critical software, &c
• In which part of the development cycle should the technology be applied?
• How did the author(s) validate the technology?

Lecture 2 - Problem frames

• Michael Jackson, "Problem Analysis and Structure," in Proceedings of NATO Summer School, Marktoberdorf, August 2000 [PDF]
• Michael Jackson, "Problem analysis using small problem frames," South African Computer Journal 22; Special Issue on WOFACS’98, pp47-60, 1999 [PDF]

Note: Treat both Jackson papers as a single reading for review.

Lecture 3 - Introduction to Alloy

• Rob Seater and Greg Dennis, "Alloy 2.0 Tutorial" (This is an interactive web site).
• MIT Software Design Group, "Micromodels of software: Lightweight modelling and analysis with Alloy" (Alloy Reference Manual) [PDF].

You should go through the Alloy tutorial, which includes downloading and running the Alloy tool. We'll be using Alloy in Assignment 1, so the tutorial will give you needed practice. (If you have problems downloading or running Alloy, please post a message to the mailing list, since other students will likely have the same problem.) You should also skim the reference manual, which covers the language constructs in more detail. Both the tutorial text and reference manual have bugs and omissions, but we can work around them.

Again, treat both documents as a single reading to review.

Lecture 4 - Alloy case studies

• Daniel Jackson. "Railway safety". (A quick note on modeling) [PDF].
• Sarfraz Khurshid and Daniel Jackson. "Exploring the Design of an Intentional Naming Scheme with an Automatic Constraint Analyzer." 15th IEEE International Conference on Automated Software Engineering (ASE 2000), September 2000. [PDF]
• Mana Taghdiri. "Analyzing multicast key management schemes". Master's Thesis, Massachusetts Institute of Technology, 2002. [PDF]

You don't need to read the entire master's thesis cover to cover. Concentrate on Chapter 4 and skim Chapters 5 and 6. You should read these papers not for their subject matter but as examples of uses of Alloy (and as validation of Alloy as a tool).

Lecture 5 - Introduction to Spin

• "Basic Spin manual".

You might also want to become familiar with the Spin web site and download the Spin tools in preparation for the next assignment.

Lecture 6 - Spin case studies

• P. Maggi and R. Sisto, "Using SPIN to verify security properties of cryptographic protocols," 9th Spin Workshop [PDF]
• Shin Nakajima and Tesuo Tamai, "Behavioral analysis of the Enterprise JavaBeans(tm) component architecture", 8th Spin Workshop [PDF].

Lecture 7 - Process calculi and refinement

• Cedric Fournet, Tony Hoare, Sriram K. Rajamani, and Jakob Rehof. "Stuck-free conformance." To appear in CAV 2004. (See me for a copy.)

Lecture 8 - Practice using refinement

• Zing language specification. [Doc]
• Zing user's manual. [Doc]

Lecture 9 - Hoare logic, weakest preconditions 1

• C.A.R. Hoare, "An axiomatic basis for computer programming," Communications of the ACM 12(10):576-580. [PDF]

Lecture 10 - Hoare logic, weakest preconditions 2

• Edsger W. Dijkstra, "Guarded commands, nondeterminacy and formal derivation of programs," Communications of the ACM 18(8):453-457. [PDF]

Lecture 11 - ESC/Java, JML

• Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata, "Extended static checking for Java", Proceedings of PLDI 2002 [PS]
• Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph R. Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll, "An overview of JML tools and applications" [PDF]

Lecture 12 - Modules and decomposition

• D.L. Parnas, "On the criteria to be used in decomposing systems into modules", Communications of the ACM 15(12):1053-1058. [PDF]

Lecture 13 - Crosscutting concerns

• P. Tarr, H. Ossher, W. Harrison, S.M. Sutton, Jr. "N Degrees of Separation: Multi-Dimensional Separation of Concerns", ICSE 1999. [PDF] Read only chapter 1 and 2.
• G. Kiczales et al. "An Overview of AspectJ", ECOOP 2001. [PDF] Read chapter 1-3 and skim other chapters.

Lecture 14 - Software architecture

• David Garlan and Mary Shaw. "An introduction to software architecture." In V. Ambriola and G. Tortora (ed.), Advances in Software Engineering and Knowledge Engineering, Series on Software Engineering and Knowledge Engineering, Vol 2, World Scientific Publishing Company, Singapore, pp. 1-39, 1993. Also available as: Carnegie Mellon University Technical Report CMU-CS-94-166, January 1994. Reprinted in "CMIS 460: Software Design and Development Faculty Course Guide", University of Maryland, Office of Instructional Development, Summer 1995. [PDF]

  Do not be intimidated by the number of pages. The typeface is huge, and the report is an easy read.

Lecture 15 - Design patterns

• Coad, "Object-oriented patterns", CACM 35(9)[PDF]

Lecture 16 - Implicit invocation

• Garlan, Jha, Notkin and Dingel, "Reasoning about implicit invocation", ICSE '98[PDF]

Lecture 17 - Testing 1

• Charles Mann, "Why software is so bad", MIT Technology Review, Jul/Aug 2002.
• Lev Nachmanson, Margus Veanes, Wolfram Schulte, Nikolai TIllmann, and Wolfgang Grieskamp, "Optimal strategies for testing nondeterministic systems," ISSTA 04 [PS].

Lecture 18 - Testing 2

• Tom Ball, "A theory of predicate-complete test coverage and generation," Microsoft Research Tech Report MSR-TR-2004-28, [PDF]