Abstract
Detecting faults in specifications can help reduce the cost and risk of software development because incorrect implementation can be prevented early. This goal can be achieved by verifying the consistency and validity of specifications. In this paper we put forward specification testing as a practical technique for verification and validation of formal specifications. Our approach is to derive proof obligations from a specification and then test them, in order to detect faults leading to the violation of consistency or validity of the specification. We describe proof obligations for various consistency properties of a specification, and suggest the use of five strategies for testing them. We provide a method for testing implicit specifications by evaluation rather than by prototyping, and criteria for interpreting the meaning of test results.
This work is supported in part by the Ministry of Education of Japan under Grant- in-Aid for Scientific Research on Priority Areas (A) (No. 09245105), Grant-in-Aid for Scientific Research (B) (No. 11694173), and Grant-in-Aid for Scientific Research (C) (No. 11680368)
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
B.W. Boehm. Software Engineering Economics. Prentice-Hall, 1981.
R. A. Kemmerer. Testing Formal Specifications to Detect Design Errors. IEEE Transactions on Software Engineering, SE-11(1):32–43, January 1985.
Cliff B. Jones. Systematic Software Development Using VDM. Prentice-Hall International (UK) Ltd., 1990.
Antoni Diller. Z: An Introduction to Formal Methods. John Wiley & Sons, 1994.
Lee J. White. Software Testing and Verification, volume 26. Academic Press, ADVANCES IN COMPUTERS, 1987.
Roger. Duke, Gordon Rose, and Gordon Smith. Object-Z: a Specification Language Advocated for the Description of Standards. Computer Standards and Interfaces, 17:511–533, 1995.
Jian Chen and Shaoying Liu. An Approach to Testing Object-Oriented Formal Specifications. In Proceedings of the International Conference TOOLS Pacific 96: Technology of Object-Oriented Languages and Systems, Melbourne, November 1996. TOOLs/ISE.
I. J. Hayes. Specification Directed Module Testing. IEEE Transactions on Software Engineering, SE-12(1):124–133, January 1986.
Marie Claude Gaudel Gilles Bernot and Bruno Marre. Software Testing based on Formal Specifications: a Theory and a Tool. Software Engineering Journal, pages 387–405, November 1991.
P. Stocks and D. Carrington. A framework for specification-based testing. IEEE Transactions on Software Engineering, 22(11):777–793, November 1996.
Shaoying Liu, A. Jeff Offutt, Chris Ho-Stuart, Yong Sun, and Mitsuru Ohba. SOFL: A Formal Engineering Methodology for Industrial Applications. IEEE Transactions on Software Engineering, 24(1):337–344, January 1998. Special Issue on Formal Methods.
Shaoying Liu, Masashi Asuka, Kiyotoshi Komaya, and Yasuaki Nakamura. An Approach to Specifying and Verifying Safety-Critical Systems with Practical Formal Method SOFL. In Proceedings of Fourth IEEE International Conference on Engineering of Complex Computer Systems (ICECCS’98), pages 100–114, Monterey, California, USA, August 10-14 1998. IEEE Computer Society Press.
Shaoying Liu, Masaomi Shibata, and Ryuichi Sato. The Specification, Design and Implementation of a University Information System. Technical Report HCU-IS-99-005, Hiroshima City University, 1999.
Kevin Lano. The B Language and Method: A Guide to Practical Formal Development. Springer-Verlag London Limited, 1996.
Chris Ho-Stuart and Shaoying Liu. A Formal Operational Semantics for SOFL. In Proceedings of the 1997 Asia-Pacific Software Engineering Conference, pages 52–61, Hong Kong, December 1997. IEEE Computer Society Press.
Carroll Morgan. Programming from Specifications. Prentice-Hall International (UK) Ltd., 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Liu, S. (1999). Verifying Consistency and Validity of Formal Specifications by Testing. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1708. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48119-2_49
Download citation
DOI: https://doi.org/10.1007/3-540-48119-2_49
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66587-8
Online ISBN: 978-3-540-48119-5
eBook Packages: Springer Book Archive