Computer System/Software Verification and Validation - course outline – rev 1
Calendar Description: Formal techniques: proving programs correct, checking consistency and completeness. Inspections and reviews. Unit/module testing. White box and black box testing. System integration and testing. Tool support for testing. Faults vs. failures. Verification of implementation against both requirements and design. Techniques for critical software. Trustworthiness vs. reliability. Timing analysis and verification. Safety analysis. Multi-version programming. Software quality assurance, software reliability. Debugging.
Instructor: Dr. C.D. (Terry) Shepard
Home: 541 0631
RMC: 541 6000, x6031; shepard@rmc.ca; RMC office: Sawyer 4019
Queen's:
shepard@qucis.queensu.ca, Queen’s office: Goodwin 623The course will meet regularly for at most 12 weeks, once a week for 3 hours on Tuesdays, starting at noon, in Goodwin 521at Queen’s. The first meeting is 12 January 1999. One or two of these meetings are likely to involve guest speakers. The duration of the course is 16 weeks, counting the break week and the 3 weeks from the Queen’s end of classes to the end of the exam period. Student presentations will be made during the course, with a major presentation at the end of the course. Regular lectures in the course will end no later than 9 April. There may still be guest lectures after that time. There will be no class meetings during the Queen’s reading week, 22-28 February, but the class will meet during the RMC break week.
There will be three assignments. The first will involve regression testing of a small system called ‘Grades’. One of the aspects of that testing will be the use of a simple object-oriented unit testing tool called pgmgen. The second assignment will involve evaluation of a commercial testing tool such as Rational’s Testmate. The exact choice is subject to availability and must be negotiated with the instructor. Other verification tools, such as the Eves formal verification environment can be considered as well. The third assignment will be a presentation to the class and a paper on a topic to be negotiated with the instructor. The paper can consist of annotated copies of the slides used for the presentation. Sample papers from past years are available. Students are expected to complete the recommended reading assignments each week, and be prepared to discuss them in class. There may be a final exam.
Note that the order in which the topics are presented in the course is determined by the needs of the course, and does not correspond to the order in which V&V activities would be carried out in real projects.
Detailed Course Outline
It would be nice to have a preprinted collection of reading material for this course. Because of the large volume of papers of interest, and because the main references keep changing every year, and because of the difficulties of obtaining copyright approvals for the Queen's Printer, this is unfortunately not worth doing at the moment.
General references (there is no one text for the course)
Fred Brooks, The Mythical Man-Month: Essays on Software Engineering, Addison Wesley, 1975, reprinted with corrections, 1982, 20th Anniversary edition with added material, 1996
Fred Brooks, No Silver Bullet: Essence and Accidents of Software Engineering, IEEE Computer 20,4, Apr. 1987
Roger S. Pressman, Software Engineering, 4th Edition, McGraw Hill, 1997
Nancy Leveson, Safeware, Addison Wesley, 1995
Peter Neumann, Computer-Related Risks, Addison Wesley, 1995
- see also CACM Risks column, Risks newsgroup, Risks in ACM SEN
Week 1: Presentation and discussion of course outline. V&V overview. Hoffman and Strooper view of software design, testing and maintenance. Assignment 1: Regression testing of ‘Grades’
V&V must be an integral part of any software development process, from the very beginning of the process. It is estimated that 40% to 70% of software development costs are spent for error detection and removal. Correctness is in this sense the most fundamental of all the quality attributes software may possess. The other attributes are much less significant as cost centres, and may even provide a net cost benefit if they are well managed. All that can be done with error control is to reduce its cost and impact.
The greatest benefits are derived from early attention to V&V. By some estimates, half of all defects originate in requirements, and another one quarter in design. Defects from these work products become increasingly costly to find and repair as they propagate to later work products – sometimes by a factor of 100. This suggests that the most important V&V activity is to enforce rigourous requirements and design processes. It is also true that many defects are introduced during the transition from one representation to another, so a second major V&V activity is to search for ways to minimize the need for such transitions. In spite of the importance of these factors, we will spend little time in this course on them. Our focus will be on inspection and testing, and to some extent on the use of mathematical techniques.
Assignment 1 is based on the ‘Grades’ system, initially developed by students at the University of Victoria, and modified both at U Vic and at RMC. You will need basic familiarity with simple mathematical logic expressions, Unix, Makefiles, C and shell scripts. There are a number of known faults in the Grades work products, and there are undoubtedly other faults yet to be found. It would be an interesting exercise to classify the faults according to severity. You are encouraged to attempt this as extra work for Assignment 1. You are also encouraged to track your own use of time in completing Assignment 1, and to report this use, again as extra work for Assignment 1.
Reference:
Hoffman, Dan and Strooper, Paul, Software Design, Automated Testing, and Maintenance, International Thompson Computer Press, 1995
(text for RMC EEE/GEF 491a:
Week 2: The object-oriented testing tool pgmgen. Ariane-5 case study. Introduction to Software Quality
Background and preparation:
pgmgen was developed at the University of Victoria. Copies are on line at RMC and at Queen’s. Described in Hoffman and Strooper (above). pgmgen is not useful other than for teaching purposes. The original reference for pgmgen is: Dan Hoffman, "A CASE Study in Module Testing", 1989 Conference on Software Maintenance, October 1989, Miami, Florida
Mark Dowson, "The ARIANE 5 Software Failure", ACM SEN, v. 22 n.2, Mar 97, pp. 84
Ariane 5 Commission of enquiry report (available at www.cnes.fr)
Jean-Marc JJ zJ quel, Bertrand Meyer, "Design by Contract: The Lessons of Ariane", IEEE Computer, v. 30 n.1, Jan 97, pp. 129-130
Read for presentation and discussion:
January 1996 IEEE Software: theme issue on Software Quality
Introductory article: Barbara Kitchenham and Sherry Lawrence Pfleeger, "Software Quality: The Elusive Target", pp 12-21
W.Robert Collins, Keith W. Miller, Bethany J. Spielman and Phillip Wherry, "How Good is Good Enough?", Communications of the ACM, Jan. 1994, pp. 81-91
Week 3: Software quality overview. Quality Models. ISO 9000. CMM. Sample IEEE SW Quality Standards. The V&V Process. V&V plans: IEEE Standard 1012-1986, 1998 revision. A Sample Safety Critical Software Standard. Introduction to Inspection.
Background and preparation:
Software Quality Models: McCall (1977), ISO 9126 (1991)
Some IEEE Standards related to quality:
IEEE 730: Software QA Plans
IEEE 982: Dictionary of measures to produce reliable software
IEEE 1061: Software quality metrics methodology
IEEE 1228: Software safety plan
IEEE 1298: Software quality management system (Part 1)
IEEE 1012: Software V&V Plans
- proposed revision of 1012 now available as an official 1998 draft.
ISO 9000 QA Standards
ISO 9001 applies to engineering
ISO 9000-3 applies to software engineering
James Moore, Software Engineering Standards: A User's Road Map, IEEE CS Press, 1998, 304 pp
- For more discussion of the complex and messy world of software standards
CANDU Computer Systems Engineering Centre of Excellence, Standard for Software Engineering of Safety Critical Software, CE-1001-STD, Ontario Hydro, Toronto, 1990; rev 1. 1995
Mike Viola, Ontario Hydro’s Experience with New Methods for Engineering Safety Critical Software (SAFECOMP 95)
Read for presentation and discussion:
M.E. Fagan "Design and Code Inspections to Reduce Errors in Program Development", IBM Systems Journal, March 1976, vol.15, no.3, pp.105-211
- the original paper showing the importance of inspections
M.E. Fagan "Advances in Software Inspections", IEEE Transactions on Software Engineering, vol. SE-12,no.7, pp.744-751, 1986
Glen W. Russell, "Experience with Inspection in Ultralarge-Scale Developments", IEEE Software, January 1991, pp. 25-31
- BNR introducing inspections 20 years after IBM
Week 3: Books on Software Quality:
Joc Saunders and Eugene Curran, Software Quality, A Framework for Success in Software Development and Support, Addison Wesley/ACM Press, 1994
This book provides an overview of the current (as of 1994) state of the practice in terms of the application of standards to the software development process. It prescribes essential steps that must be taken, but only in general terms, leaving the technical details to be filled in elsewhere.
G. Gordon Schulmeyer and James I. McManus, Eds, Total Quality Management for Software, Van Nostrand Reinhold, 1992
The authors are all industrially based, which gives this book a very different orientation from books by professors. It appears to cover all the important issues with respect to building quality software. The SEI CMM (see list of additional references) is given prominence, but little is said about ISO 9000 - the emphasis is on the TQM ideas of Deming.
Donald C. Gause & Gerald M. Weinberg, "Exploring Requirements: Quality before design", Dorset House Publishing, 1989
Gilb, Tom, Principles of Software Engineering Management, Addison Wesley, 1988
Week 4 (revised): Introduction to Inspection and Reviews.
Background and preparation:
Videotape: Glen Russell: Code Inspection; BNR, Feb. 1993
This is available strictly for educational purposes; the notes that accompany the tape are also available. It was developed as part of an inspection training program at BNR, and is perhaps most effective if used as part of the whole day training. It shows a good inspection meeting and a bad one, and gives an example of good paraphrasing and bad. The paraphrasing example may be of greatest value, but some preparation is needed to follow it.
Notes from presentation on inspections by John Botsford of IBM to EE 591 in the Fall term of 1993/94 are available (copies made for all students).
Read for presentation and discusssion:
David Parnas and David Weiss, Active Design Reviews: Principles and Practices, J. of Systems and Software, n. 7, 1987, pp. 259-265
and
Edward F. Weller, "Lessons from Three Years of Inspection Data", IEEE Software, v. 10 n.5, Sep 1993, pp. 38-45 [Best article for 93]
A. Porter, H. Siy, C.A. Toman, L.G. Votta, "An Experiment to Assess the Cost-Benefits of Code Inspections in Large Scale Software Development", ACM SEN, v. 20 n.4, Oct 1995, pp. 92-103 [need to bring ref. up to date – experiment is now complete: IEEE TSE June 97 pp. 329-346, v.23 n. 6] (choice in 1999)
or
Adam A. Porter, Lawrence G. Votta, Victor R. Basili, "Comparing Detection Methods for Software Requirements Inspections: A Replicated Experiment", IEEE TSE, v. 21 n.6, Jun 1995, pp. 563-575 (not done in 1999)
Week 5 (revised): Assignment 1 due. Continuation of Inspection Overview. Checklists (Myers, Kaner). Defect Causal Analysis. Personal Software Reviews. Start of Assignment 2: Discussion of Rational Testmate
Rational Apex and Testmate are available on RMC and Queen’s Sun workstations. Rational also has other testing tools (such as Pure tools, Visual Test, SQA, …) which are worth investigating.
Read for presentation and discussion:
Pick a book on testing , read it enough to form an opinion, and come to the class prepared to spend 10 minutes giving your opinion.
Books on testing:
Boris Beizer, Software Testing Techniques, van Nostrand Reinhold, 1983, 2nd Edition, 1990
about twice as long as the 1st Edition. There is a problem with this book, in that it largely ignores the strong evidence in favour of doing inspection before testing. The reason is that this is a book written from experience in the trenches over the past 20+ years, during which time inspection was still not widely used
Boris Beizer, Black Box Testing, Wiley, 1995
Richard A. DeMillo, W. Michael McCracken, R.J. Martin, and John F. Passafiume, Software Testing and Evaluation, Benjamin Cummings, 1987
Paul C. Jorgensen, Software testing: a craftsman's approach, CRC Press, 1995, 0-8493-7345-X
Cem Kaner, Jack Faulk, and Hung Quoc Nguyen, Testing Computer Software, 2nd Edition, VanNostrand, 1993
Covers legal issues as well as technical issues – Kaner is a lawyer as well as a Ph.D in CS from McMaster.
Edward Kit, Software Testing in the Real World: Improving the Process, Addison Wesley, 1995
Management orientation, but also a good overview of some technical issues.
Brian Marick, The Craft of Software Testing, Prentice Hall, 1995
- one man’s very personal view of testing
G.J. Myers, The Art of Software testing, Wiley, 1979
Still a widely used book. Short, sensible, covers a number of issues and techniques that are still current.
William Perry, Effective Methods for Software Testing, Wiley-QED, 1995
William E. Perry & Randall W. Rice, Surviving the Top Ten Challenges of Software Testing: A People-Oriented Approach, Dorset House, 1997
Marc Roper, Software Testing, McGraw Hill, 1994, 149 pp
- short, sensible, and expensive
Thomas Royer, Software Testing Management: Life on the Critical Path, Prentice-Hall, Englewood Cliffs, NJ, 1993
Reviewed in IEEE Software May 94, pp. 114-115; orientation toward testing by US DoD; has some dubious parts, but generally solid - only 230 pages; also positively reviewed in IEEE Computer, Mar. 94, p126
Systems Testing and Quality Assurance Techniques, Advanced Information Technologies, Course notes from Mike Nedvidek’s participation in the course, Jan. 1997
Stewart Gardiner, Ed. "Testing Safety-Related Software: A Practical Handbook", Springer-Verlag, 1998
Week 6: Orthogonal Defect Classification. Overview of Testing. Lists of test tools. Testing Maturity Model.
R. Chillarege, et al., "Orthogonal Defect Classification - A Concept for In-Process Management", IEEE TSE, v. 18 n.11, Nov 92, pp. 943-956
Overview of testing: Professor’s notes.
Test tools from a number of companies are available for evaluation. Examples include ParaSoft’s Codewizard source code analysis tool, and User Interface testing tools such as Xrunner Also see letter describing problems with such tools, pp. 12,14, IEEE Software Nov/Dec 97. Pointers to sites on web will be available at
www.cs.queensu.ca/home/shepard/testingRobert M. Poston & Michael P. Sexton, "Evaluating and Selecting Testing Tools", IEEE Software, v. 9 n.3, May 1992, pp. 33-42
Robert M. Poston, "Testing Tools Combine Best of New and Old", IEEE Software, v. 12 n.2, Mar 1995, pp. 122-126
Read for presentation and discussion:
Ilene Burnstein, Taratip Suwannasort, C.R. Carlson, "Developing a Testing Maturity Model …", STSC Crosstalk, v. 9 Part I: n.8 Aug 96, pp. 21-24, and Part II: n9, Sep 96, pp. 19-26 (available at stsc.hill.af.mil/SWTesting/index.html)
Gregory Daich, "Emphasizing Software Test Process Improvement", STSC Crosstalk, v. 9, n.6, Jun 96 (available at stsc.hill.af.mil/SWTesting/index.html)
Pick a book on testing.
Week 7: Strategies for selecting test cases. Test Automation. Automatic generation of tests.
Robert M. Poston, Automating Specification Based Software Testing, IEEE CS Press, 1996
Victor Basili and Richard Selby, Comparing the Effectiveness of Software Testing Strategies, IEEE TSE, Dec. 1987
Read for presentation and discussion:
D. Hamlet and R. Taylor, Partition Testing does not inspire Confidence, IEEE TSE, Dec. 1990, pp. 1402-1411
John B. Goodenough, Susan Gerhart, Toward a Theory of Test Data Selection, IEEE TSE, 1975, pp. 156-173, v. 1
Week 8: Test Coverage. Test Adequacy. Regression testing. Report on ISSTA 98.
Joseph R. Horgan, Saul London, "Achieving Software Quality with Testing Coverage Measures", IEEE Computer, v. 27 n.9, Sep 1994, pp. 60-69
Hong Zhu, "A Formal Analysis of the Subsume Relation Between Software Test Adequacy Criteria", IEEE TSE, v. 22 n.4, Apr 96, pp. 248-255
Report on ISSTA 98: Professor’s notes. Proceedings are available in RMC library
Hareton K. Leung and Lee White, "Insights into Regression Testing", Conference on Software Maintenance, IEEE, pp. 60-69, 1989
Read for presentation and discussion:
Gregg Rothermel, Mary Jean Harrold, "A Safe, Efficient Regression Test Selection Technique", ACM TOSEM, v. 6 n.2, Apr 97, pp. 173-210
Week 9: Object-oriented testing. Ideas for a testing framework for ObjecTime. Languages for describing tests. State space techniques for protocol testing. TTCN. Assignment 2 due.
David C. Kung, Pei Hsia, and Jerry Gao, Testing Object-Oriented Software, IEEE CS Press, 1998
Ideas for a testing framework for ObjecTime: Professor’s notes.
The basic reference for ObjecTime is :
Bran Selic, Garth Gullekson & Paul Ward, Real-Time Object Oriented Modeling, Wiley, 1994
The current version of the Objectime tool, Developer 5.2, is available at RMC and at Queen’s. They have recently added a layered product for testing, called Testscope, which should be available on line soon.
Richard J. Linn and M. Ümit Uyar, "Conformance Testing Methodologies and Architectures for OSI Protocols", IEEE CS Press, 1994
Read for presentation and discussion:
Robert L. Probert and Oz Monkewich, TTCN: The International Notation for Specifying Tests of Communications Systems, Computer Networks 23,5; 1992 pp. 417-438
Week 10: When to stop testing. Software reliability. Operational Profiles. Safety and Trustworthiness. Guest presentation by Diane Kelly of Ontario Hydro.
Jesse H. Poore, Harlan D. Mills, David Mutchler, "Planning and Certifying Software System Reliability", IEEE Software, v. 10 n.1, Jan 1993, pp. 88-99 [Runner up for best article of 93]
E.N. Adams, "Optimizing Preventive Service of Software Products", IBM J.R&D, Jan 84, [The original data to support the use of operational profiles]
Denise Woit, "Operational Profile Specification, Test Case Generation, and Reliability Estimation for Modules", Ph.D. Thesis, Queen's University, January 1994.
Praerit Garg, "Investigating Coverage-Reliability Relationship and Sensitivity of Reliability to Errors in the Operational Profile" Cascon 94 (Garg was a Ph.D student at Purdue at the time)
Theme Issue: "System Testing and Reliability", IEEE Computer, v. 29 n.11, Nov 96, pp. 28-86 [SigSoft '96: 4th Symposium on the Foundations of Software Engineering]
Hazard Analysis Techniques: Ch. 14, Nancy Leveson, Safeware, Addison Wesley, 1995
Read for presentation and discussion (selection of at most one):
R.W. Butler and G.B. Finelli, The Infeasibility of Quantifying the Reliability of Life-Critical Real-Time Software, IEEE TSE 19(1) pp. 3-12 (Jan 93)
W.E. Howden, Yudong Huang, "Software Trustability Analysis", ACM TOSEM, v. 4 n.1, Jan 95, pp. 36-64 [use of guided testing to overcome the limitations of random testing]
The N-Version debate: does it improve reliability?
Susan Brilliant, John C. Knight & Nancy Leveson, The Consistent Comparison Problem in N-Version Software, IEEE TSE Nov. 89, pp. 1481-1485
Avizienis et al, Multi-version software development, UCLA CSD report 880034 (SEN Jul88, p56)
Week 11: Debugging. Assertion based verification. Cleanroom.
Jeffrey J.P. Tsai and Steve J.H. Yang, "Monitoring and Debugging of Distributed Real-Time Systems", IEEE CS Press, 1995
Excerpts from: Cleanroom Software Technology Centre, Cleanroom Software Engineering for Zero-Defect Software, IBM, May 31, 1992 (Overheads from a workshop sponsored by the US NSF, held at the Rochester Institute of Technology, May 31-June 4, 1992)
Monica Brockmeyer, Farnam Jahanian, Constance Heitmeyer, Bruce Labaw, "An Approach to Monitoring and Assertion-Checking of Real-Time Specifications", ACM/IEEE Proceedings, 4th Int'l workshop on Parallel and Dist'd Real-Time Systems, Apr 96, pp. 236-243 [Modechart; also paper at RTAS 97, on testing RT specs. pp. 125-135]
Read for presentation and discussion (1 or 2 to be selected):
S. Wayne Sherer, Ara Kouchakdjian, "Experience Using Cleanroom Software Engineering", IEEE Software, v. 13 n.3, May 96, pp. 69-76 [Picatinny Arsenal]
D.S. Rosenblum, "A Practical Approach to Programming with Assertions", IEEE TSE, v. 21 n.1, Jan 95, pp. 19-31 [Correction: p. 265, Mar 95 IEEE TSE]
Beth A. Schroeder, "On-Line Monitoring: A Tutorial", IEEE Computer, v. 28 n.6, Jun 95, pp. 72-78
Week 12: Formal verification of software work products. Eves. Requirements and Design based checking. (e.g. SCRtool V&V capabilities) Measuring Design Quality. Model Checking.
Will Tracz, "Test and Analysis of Software Architectures", ACM SEN, v. 21 n.3, May 96, pp. 1-3 [ISSTA 96 Proceedings: Keynote address summary]
J.M. Wing, A Specifier's Introduction to Formal Methods. IEEE Computer, 23(9):8-24, September 1990
James H. Fetzer, Program Verification: The Very Idea, CACM, Sept 1988; comments CACM Apr 89 p. 420
Anya Malton and Terry Shepard, "A Beginner's Manual for Eves", RMC, Jan 93, revised Jan 1994 by Dave Andrews
Constance L. Heitmeyer, Ralph D. Jeffords, Bruce G. Labaw, "Automated Consistency Checking of Requirements Specifications", ACM TOSEM, v. 5 n.3, July 96, pp. 231-261
J.A. Hall, Seven Myths of Formal Methods. IEEE Software, 7(5):11-19, September 1990.
J.P. Bowen and M.G. Hinchey, Seven More Myths of Formal Methods. IEEE Software, 12(4):34-41, July 1995.
J.P. Bowen and M.G. Hinchey, Ten Commandments of Formal Methods. IEEE Computer, 28(4):56-63, April 1995.
R. E. Bryant, ``Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams,'' ACM Computing Surveys, Vol. 24, No. 3 (September, 1992), pp. 293-318.
Read for presentation and discussion:
Dan Craigen, Susan Gerhart and Ted Ralston, "Formal Methods Technology Transfer: Impediments and Innovation", In Applications of Formal Methods. ed. M. G. Hinchey and J. P. Bowen. Prentice-Hall International Series in Computer Science, September 1995. (23 pages)
An innovation diffusion model is used to analyze the data collected during an international survey of industrial applications of formal methods. The model provides a structured means for determining the likely adoption trajectory of formal methods. We conclude that formal methods will only be slowly diffused into industry and provide examples and recommendations on how to ease impediments to diffusion.
Anthony Hall, "Using Formal Methods to Develop an ATC Information System", IEEE Software, v. 13 n.2, Mar 96, pp. 66-76
Weeks 13 to 15: April 13, 20, 27 will be used for student presentations (which will need at least two 3 hour slots) and perhaps for a guest lecture or for additional time to discuss the first two assignments. As well, if a final exam is needed for some students, it will be scheduled in that time period.
Examples of possible student projects (copies of papers/presentations are available from past years):
Evaluation of a commercially available testing tool other than Testmate
EVES/Verdi/NEVER or another program proof of correctness tool, using model checking in particular.
Usability Testing
In depth presentation of a selection of papers on any of the areas covered in the course