Inspections of formal specifications

ABSTRACT

This paper describes a student peer review process that has been incorporated within an introductory course in formal methods. As a course project, a team of students develops a formal specification of the requirements for a software system. The final part of the project involves the inspection of the specification by another team of student reviewers. The paper presents a rationale for including inspections as part of a formal methods course. It provides a detailed description of the inspection process and reports on the application of the process to a specific class project. Finally, the paper assesses the results of the use of such a paradigm and discusses how to improve it.

REFERENCES

• 1: Antoni Diller, Z: An Introduction to Formal Methods, John Wiley & Sons, Inc., New York, NY, 1994
• 2: Raymond Dion, Process Improvement and the Corporate Balance Sheet, IEEE Software, v.10 n.4, p.28-35, July 1993 [doi>10.1109/52.219618]
• 3: Fagan, ME., "Design and Code Inspections to Reduce Errors m Program Development", IBM ~S~vstems .}our~lal,, Vol 15, No. 3, 1976, pp. 186- 211.
• 4: Robert G. Ebenau , Susan H. Strauss, Software inspection process, McGraw-Hill, Inc., New York, NY, 1993
• 5: Susan Gerhart , Dan Craigen , Ted Ralston, Experience with Formal Methods in Critical Systems, IEEE Software, v.11 n.1, p.21-28, January 1994 [doi>10.1109/52.251198]
• 6: Thomas B. Hilburn , Iraj Hirmanpour , Andrew J. Kornecki, The Integration of Software Engineering into a Computer Science Curriculum, Proceedings of the 8th SEI CSEE Conference on Software Engineering Education, p.87-97, March 29-April 01, 1995
• 7: Watts S. Humphrey, Managing the software process, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1989
• 8: IEEE Software Staff, Process-Oriented Software Education, IEEE Software, v.11 n.6, p.99-101, November 1994 [doi>10.1109/52.329412]
• 9: Peter G. Neumann, System development woes, Communications of the ACM, v.36 n.10, p.146, Oct. 1993 [doi>10.1145/163430.164065]
• 10: Mark C. Paulk , Bill Curtis , Mary Beth Chrissis , Charles V. Weber, Capability Maturity Model, Version 1.1, IEEE Software, v.10 n.4, p.18-27, July 1993 [doi>10.1109/52.219617]
• 11: Roger S. Pressman, Software engineering (3rd ed.): a practitioner's approach, McGraw-Hill, Inc., New York, NY, 1992

INDEX TERMS

Primary Classification:
  K. Computing Milieux
  K.3 COMPUTERS AND EDUCATION

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Theory