Abstract
In this article, we consider model oriented formal specification languages. We generate test cases by performing symbolic execution over a model, and from the test cases obtain a Java program. This Java program acts as a test driver and when it is run in conjunction with the implementation then testing is performed in an automatic manner. Our approach makes the testing cycle fully automatic. The main contribution of our work is that we perform automatic testing even when the models are non-deterministic.
Work done within the EU research project Rodin, IST 511599.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abrial, J.-R.: The B–Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
Bernard, E., Legeard, B., Luck, X., Peureux, F.: Generation of test sequences from formal specifications: GSM 11-11 standard case study. Software Practice and Experience 34(10), 915–948 (2004)
Colin, S., Legeard, B., Peureux, F.: Preamble computation in automated test case generation using constraint logic programming. Software Testing Verification and Reliability, John Wiley 14, 213–235 (2004)
Dick, J., Faivre, A.: Automating the Generation and Sequencing of Test Cases from Model-based Specifications. In: Larsen, P.G., Woodcock, J.C.P. (eds.) FME 1993. LNCS, vol. 670, pp. 268–284. Springer, Heidelberg (1993)
Dalal, S.R., Jain, A., Karunanithi, N., Leaton, J.M., Lott, C.M., Patton, G.C., Horowitz, B.M.: Model Based Testing in Practice. In: Proc. of ICSE 1999 (1999)
El-Far, I.K., Whittaker, J.A.: Model Based Software Testing. In: Marciniak, J.J. (ed.) Encyclopedia on Software Engineering, John Wiley, Chichester (2001)
Gannon, J.D., Hamlet, R.G., Mills, H.D.: Theory of modules. IEEE Transactions on Software Engineering 13(7), 820–829 (1987)
Garey, M.R., Johnson, D.S.: Computers and Intractability. W. H. Freeman and Company, New York (1979)
Gurevich, Y.: Sequential Abstract-State Machines Capture Sequential Programs. ACM Transaction on Computational Logic 1(1), 77–111 (2000)
Hierons, R.M.: Testing from a Non-deterministic Finite State Machine using Adaptive State Counting. IEEE Transactions on Computers 53(10), 1330–1342 (2004)
Hierons, R.M.: Applying Adaptive Test Cases to Non-deterministic Implementations. Information Processing Letters 98(2006), 56–60 (2006)
Jones, C.B.: Systematic Software Development using VDM, 2nd edn. Prentice-Hall, Englewood Cliffs (1990)
Lee, D., Yannakakis, M.: Principles and Methods of Testing Finite State Machines: A survey. Proc. of the IEEE 80(8), 1090–1123 (1996)
Legeard, B., Peureux, F., Utting, M.: Automatic Boundary Testing from Z and B. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 21–40. Springer, Heidelberg (2002)
Legeard, B., Peureux, F., Utting, M.: Controlling test case explosion in test generation from B formal models, Software Testing, Verification and Reliability, pp. 81–103. John Wiley, Chichester (2004)
Leuschel, M., Butler, M.: ProB: A Model Checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003)
Nachmanson, L., Veanes, M., Schulte, W., Tillmann, N., Grieskamp, W.: Optimal Strategies for Testing Nondeterministic Systems. In: ACM ISSTA 2004, Boston, ACM Press, New York (2004)
Panzl, D.J.: Automatic Software Test Drivers. IEEE Computer 11(4) (1978)
Richardson, D.J., Leif Aha, A., O’Malley, T.O.: Specification-based Test Oracles for Reactive Systems. In: Proc. of the 14th ICSE, Melbourne, pp. 105–118 (1992)
Satpathy, M., Butler, M., Ramesh, S., Leuschel, M.: Automatic Testing of Formal Specifications, Technical Report 792, Abo Akademi University, Turku, Finland (2006), available at: http://www.tucs.fi/publications
Satpathy, M., Leuschel, M., Butler, M.: ProTest: An Automatic Test Environment for B Specifications. Electronic Notes on TCS (ENTCS) 111, 113–136 (2005)
Spivey, J.M.: Understanding Z. Cambridge University Press, Cambridge (1988)
Yannakakis, M., Lee, D.: Testing Finite State Machines: Fault Detection. Journal of Computer and System Sciences 50, 209–277 (1995)
Zhang, F., Cheung, T.: Optimal Transfer Trees and Distinguishing Trees for Testing Observable Nondeterministic Finite State Machines. IEEE Transactions on Software Engineering 29(1), 1–14 (2003)
Zhu, H., Hall, P.A.V., May, J.H.R.: Software Unit Test Coverage and Adequacy. ACM Computing Surveys 29(4), 366–427 (1997)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Satpathy, M., Butler, M., Leuschel, M., Ramesh, S. (2007). Automatic Testing from Formal Specifications. In: Gurevich, Y., Meyer, B. (eds) Tests and Proofs. TAP 2007. Lecture Notes in Computer Science, vol 4454. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-73770-4_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-73770-4_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-73769-8
Online ISBN: 978-3-540-73770-4
eBook Packages: Computer ScienceComputer Science (R0)