Abstract
The traditional software development cycle relies mostly on informal methods to capture design errors in its initial phases, and on more rigorous testing methods during the later phases. It is well understood, though, that those bugs that slip through the early design phases tend to cause the most damage to a design. The anomaly of traditional design is therefore that it excels at catching bugs at the worst possible point in a design cycle: at the end.
In this paper we consider what it would take to develop a suite of tools that has the opposite characteristic: excelling at catching bugs at the start, rather than the end of the design cycle. Such early fault detection tools differ from standard formal verification techniques in the sense that they must be able to deal with incomplete, informal design specifications, with possibly ill-defined requirements. They do not aim to replace either testing or formal verification techniques, but to complement their strengths.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
A.V. Aho, B.W. Kernighan, P.J. Weinberger. The AWK Programming Language. Addison-Wesley, 1988.
R. Alur, G.J. Holzmann, D. Peled. An Analyzer for Message Sequence Charts. This conference. 1996.
J. Berry, N. Dean, P. Fasel, M. Goldberg, E. Johnson, J. MacCuish, G. Shannon, S. Sklena. Link: A Combinatorics and Graph theory workbench for applications and research. DIMACS, Technical Report 95-15, June 1995.
E.R. Gasner, E. Koutsofios, S.C. North, K-P. Vo. A Technique for drawing directed graphs. IEEE Trans. on Software Eng. Vol 19, No. 3, May 1993, pp. 214–230.
R. Gerth, D. Peled, M.Y. Vardi, P. Wolper. Simple On-the-fly Automatic Verification of Linear Temporal Logic, PSTV95, Protocol Specification Testing and Verification. Warsaw, Poland. Chapman & Hall, Germany, 1995, 173–184.
G.J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, Software Series, 1991.
G.J. Holzmann, D. Peled. An Improvement in Formal Verification. Proc. 7th Int. Conf. on Formal Description Techniques. Berne, Switzerland, 1994, 177–194.
J. Ousterhout. Tcl and the Tk Toolkit. Addison-Wesley, 1994.
A. Pnueli, The temporal logic of programs, Proc. of the 18th IEEE Symp. on Foundation of Computer Science. 1977, 46–57.
B. Selic, G. Gullekson, P.T. Ward. Real-time object-oriented modeling. Wiley, New York, 1994.
N.M. Wilkinson. Using CRC cards: an informal approach to object-oriented development. SIGS Books, New York, Advances in Object Technology, 1995.
ITU-T (previously CCITT). Criteria for the use and applicability of formal description techniques. Recommendation Z.120, Message Sequence Chart (MSC). March 1993, 35 pgs.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Holzmann, G.J. (1996). Early fault detection tools. In: Margaria, T., Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1996. Lecture Notes in Computer Science, vol 1055. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61042-1_34
Download citation
DOI: https://doi.org/10.1007/3-540-61042-1_34
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61042-7
Online ISBN: 978-3-540-49874-2
eBook Packages: Springer Book Archive