|
||||
University of Oregon
|
This list is not complete and some choices of papers may change.
(A) = Assigned
(O) = Optional extra reading
(A) Medical Devices: The Therac-25. Nancy Leveson. Excerpted from Safeware: System Safety and Computers, Addison-Wesley, 1995. Copyright 1995. [Hardcopy; for an electronic version visit Nancy Leveson's home page at sunnyday.mit.edu]
(O) Software Qualities. Michal Young and Mauro Pezze`. This set of course notes corresponds to my lecture on software qualities, but is in more of a "textbook" presentation of the material, including questions. I do suggest reading this, but you need not prepare a review of it. (On the other hand, I will appreciate comments since I plan to incorporate this material in a book.)
(O) Experience with Inspection in Ultralarge-Scale Developments. Glen W. Russel. IEEE Software, January 1991, pages 25-31. [Hardcopy only]
This article has a good, concise summary of the basic Fagan inspection technique, and is typical of popularized descriptions of inspections with a large dollop of marketing. Contrast it with the style of the paper by Perpich et al., which is more in the style of an academic research paper with empirical evaluation.
(A) Anywhere, Anytime Code Inspections: Using the Web to Remove Inspection Bottlenecks in Large-Scale Software Development. J. M. Perpich, D. E. Perry, A. A. Porter, L. G. Votta , and M. W. Wade.
When my students in the summer 1999 offering of OMSE 525 read this paper, they complained about its organization --- the inspection approach and details of the web-based tool are mixed together rather haphazardly. Nonetheless I think there is value in the paper, both as a modern view of the limitations and possible new approaches in inspections, and as an example (imperfect, but better than much software engineering reserach) of empirical validation.
(O) SOFTWARE FORMAL INSPECTIONS GUIDEBOOK, Office of Safety and Mission Assurance, NASA 1993. (68 pages).
Here's how at least one real organization approaches inspections, including actual check-lists. The most striking thing to me is the non-uniformity in the level of detail in these check-lists. You can learn quite a bit about software development approaches in NASA by looking at the check-lists for requirements, architecture, and design. For example, if a check-list asks whether performance trade-off studies are properly cited, you can reasonably infer that performance trade-off studies are a normal part of the development process prior to producing the kind of document covered by that check-list.
(O) An Introduction to Proving the Correctness of Programs. Sidney L. Hantler and James C. King. ACM Computing Surveys, September 1976, pp 331-353. [Hardcopy only]
(NOTE: I changed the Hantler and King paper from "assigned" to "optional".)
The technique described here is sometimes called "symbolic execution." It can be partially automated; the difficult parts to automate are simplfication of predicates and checking of assertions (which are really the same thing: an assertion is true if it simplifies to TRUE.) Although this approach to program verification is seldom practical in itself, some reasoning in this style is used in many other verification techniques, so you should understand it. As an aside, a company that produced a symbolic execution tool (although they called it something else) was recently bought by Microsoft; the tool is being used within Microsoft and is no longer being sold.
(A) The Model Checker SPIN. Gerard J. Holzmann. IEEE Transactions on Software Engineering 23(5), May 1997.
While directly proving the correctness of a paper is seldom practical, it is often possible to prove useful properties about models that have been constructed specifically for that purpose. Even though verification of the model does not guarantee that the code is correct, finding and correcting bugs in such a model is much, much easier than finding and correcting the corresponding bugs in code. One of the areas in which this approach has been most useful is verification of concurrency properties (e.g., absence of deadlock, mutual exclusion) in finite-state models of concurrent processes. Several different kinds of models of techniques have been used for this purpose; the tool SPIN uses one of the conceptually simpler approaches, which makes it a good introduction to the field. Also, it is among the most mature and practically useful of the existing finite-state verification tools.
Students in a previous class found this paper somewhat dull and difficult to read because it combines descriptions at three levels: An overview of finite-state verification, gory details of a particular finite-state verification tool, and description of applying the tool to particular examples. Unfortunately, the only other option I can think of is to read individual papers that address each of those topics. Also, since we will actually be using SPIN in an exercise this term, the nitty-gritty details about using the tool may not seem quite so useless.
(A) Aspect: Detecting Bugs with Abstract Dependence. Daniel Jackson. ACM TransactIons on Software Engineering and Methodology. 4 (2), April 1995, Pages 109-145.
(O) An Introduction to Abstract Interpretation, Samson Abramsky and Chris Hankin. In Abstract Interpretation of Functional Programs,
Butler & Finelli, Ultra-reliability TBD
(A) The category-partition method for specifying and generating fuctional tests, T. J. Ostrand and M. J. Balcer Communications of the ACM 31(6), 1988, Pages 676-686.
(A) The AETG System: An Approach to Testing Based on Combinatorial Design
David M. Cohen, Siddhartha R. Dalal, Michael L. Fredman, and Gardner C. Patton. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, VOL. 23, NO. 7, JULY 1997.
You'll see lots of similarity between AETG and category-partition testing, but AETG applies a combinatorial experimental design method (as one might use, for example, in designing a psychology experiment) to software testing.
(A) A Practical Approach to Programming with Assertions. David Rosenblum. IEEE Transactions on Software Engineering 21(1), January 1995.
Assertions are one way of implementing test oracles. They are particularly useful for unit and integration testing, less so for system testing. It is common to leave assertions in delivered software, both as an aid to debugging (an email from a user describing an assertion violation message is a lot better than "it crashed") and to force an errant application to die gracefully before it does real damage.
Bochmann, Protocol Testing TBD
