Skip to main content
SpringerLink
Log in

Testing from X-Machine Specifications

  • Chapter
Formal Methods and Testing

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 4949))

Abstract

The chapter describes how to model software containing complex data using X-machines and how test generation can be performed from such models. Testing using X-machines can be used to demonstrate specific results by testing: one may even claim that an implementation is behaviourally-equivalent to a specification if testing did not reveal defects. The ability to make such claims requires a tester to be precise in what is actually being tested and what has to be assumed. A number of assumptions underlying the testing method are described including what can be done when they cannot be satisfied.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bălănescu, T., Gheorghe, M., Ipate, F., Holcombe, M.: Formal black box testing for partially specified deterministic finite state machines. Foundations of Computing and Decision Systems 28(1) (2003)

    Google Scholar 

  2. Bogdanov, K., Holcombe, M.: Statechart testing method for aircraft control systems. Software Testing, Verification and Reliability 11(1), 39–54 (2001)

    Article  Google Scholar 

  3. Bogdanov, K., Holcombe, M.: Testing from statecharts using the Wp method. In: CONCUR 2002 Satellite Workshop on Formal Approaches To Testing (FATES), pp. 19–33 (2002)

    Google Scholar 

  4. Bogdanov, K., Holcombe, M.: Refinement in statechart testing. Software Testing, Verification and Reliability 14, 189–211 (2004)

    Article  Google Scholar 

  5. Bogdanov, K., Holcombe, M., Ipate, F., Seed, L., Vanak, S.: Testing methods for X-machines, a review. Formal Aspects of Computing 18(1) (2006)

    Google Scholar 

  6. Bochmann, G., Petrenko, A.: Protocol testing: review of methods and relevance for software testing. In: 1994 ACM International Symposium on Software Testing and Analysis (ISSTA 1994), pp. 109–124 (1994)

    Google Scholar 

  7. Cardell-Oliver, R.: Conformance tests for real-time systems with timed automata specifications. Formal Aspects of Computing 12(5), 350–371 (2000)

    Article  MATH  Google Scholar 

  8. Chow, T.: Testing software design modeled by finite-state machines. IEEE Transactions on Software Engineering SE-4(3), 178–187 (1978)

    Article  Google Scholar 

  9. Cheng, K., Krishnakumar, A.: Automatic functional test generation using the extended finite state machine model. In: ACM-SIGDA; IEEE. Proceedings of the 30th ACM/IEEE Design Automation Conference, Dallas, TX, June 1993, pp. 86–91. ACM Press, New York (1993)

    Google Scholar 

  10. Cohen, D.: Introduction to Computer Theory, 2nd edn. John Wiley & Sons, New York (1996)

    Google Scholar 

  11. Eilenberg, S.: Automata, languages and machines, vol. A. Academic Press, London (1974)

    MATH  Google Scholar 

  12. Fujiwara, S., von Bochmann, G., Khendek, F., Amalou, M., Ghedamsi, A.: Test selection based on finite state models. IEEE Transactions on Software Engineering 17(6), 591–603 (1991)

    Article  Google Scholar 

  13. Gaudel, M.: Testing can be formal, too. In: Mosses, P.D., Schwartzbach, M.I., Nielsen, M. (eds.) CAAP 1995, FASE 1995, and TAPSOFT 1995. LNCS, vol. 915, pp. 82–96. Springer, Heidelberg (1995)

    Google Scholar 

  14. Gill, A.: Introduction to the Theory of Finite-State Machines. McGraw-Hill, New York (1962)

    MATH  Google Scholar 

  15. Gunter, E., Peled, D.: Model checking, testing and verification working together. Formal Aspects of Computing 17(2), 201–221 (2005)

    Article  MATH  Google Scholar 

  16. Hierons, R., Harman, M.: Testing conformance of a deterministic implementation against a non-deterministic stream X-machine. Theoretical Computer Science 4, 191–233 (2004)

    Article  MathSciNet  Google Scholar 

  17. Holcombe, M., Ipate, F.: Correct Systems: building a business process solution. Springer, Heidelberg (1998)

    MATH  Google Scholar 

  18. Hierons, R.: Testing from a nondeterministic finite state machine using adaptive state counting. IEEE Trans. Computers 53(10), 1330–1342 (2004)

    Article  Google Scholar 

  19. Harel, D., Naamad, A.: The STATEMATE Semantics of Statecharts. ACM Transactions on Software Engineering and Methodology 5(4), 293–333 (1996)

    Article  Google Scholar 

  20. Hierons, R., Ural, H.: Reduced length checking sequences. IEEETC: IEEE Transactions on Computers 51, 1111–1117 (2002)

    Article  MathSciNet  Google Scholar 

  21. IF tool (2006), http://www-verimag.imag.fr/~async/IF/

  22. Ipate, F., Holcombe, M.: An integration testing method that is proved to find all faults. International Journal of Computer Mathematics 63, 159–178 (1997)

    Article  MATH  MathSciNet  Google Scholar 

  23. Ipate, F., Holcombe, M.: Generating test sequences from non-deterministic generalized stream X-machines. Formal Aspects of Computing 12(6), 443–458 (2000)

    Article  MATH  Google Scholar 

  24. Ipate, F., Holcombe, M.: Testing conditions for communicating stream X-machine systems. Formal Aspects of Computing 13(6), 431–446 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  25. Ipate, F.: Complete deterministic stream X-machine testing. Formal Aspects of Computing 16(4), 374–386 (2004)

    Article  MATH  Google Scholar 

  26. Inan, K., Ural, H.: Efficient checking sequences for testing finite state machines. Information and Software Technology 41, 799–812 (1999)

    Article  Google Scholar 

  27. Kozen, D.: A completeness theorem for Kleene algebras and the algebra of regular events. Information and Computation 110(2), 366–390 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  28. Larsen, K., Mikucionis, M., Nielsen, B.: Online testing of real-time systems using Uppaal. In: Grabowski, J., Nielsen, B. (eds.) FATES 2004. LNCS, vol. 3395, pp. 79–94. Springer, Heidelberg (2005)

    Google Scholar 

  29. Luo, G., Petrenko, A., von Bochmann, G.: Selecting test sequences for partially specified nondeterministic finite state machines. In: IFIP Seventh International Workshop on Protocol Test Systems, Japan, pp. 95–110 (1994)

    Google Scholar 

  30. Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines – A survey. In: Proceedings of the IEEE, August 1996, vol. 84, pp. 1090–1123 (1996)

    Google Scholar 

  31. McGregor, J.D., Korson, T.D.: Integrated object-oriented testing and development processes. Communications of the ACM 37(9), 59–77 (1994)

    Article  Google Scholar 

  32. Myers, G.: The art of software testing. John Wiley and Sons, Chichester (1979)

    Google Scholar 

  33. Ostrand, T.J., Balcer, M.J.: The category-partition method for specifying and generating functional tests. Communications of the ACM 31(6), 676–686 (1988)

    Article  Google Scholar 

  34. OMG. Unified Modeling Language specification, version 1.5 (March 2003), http://www.omg.org/technology/documents/formal/uml.htm

  35. Petrenko, A., Boroday, S., Groz, R.: Confirming configurations in EFSM testing. IEEE Transactions on Software Engineering 30(1), 29–42 (2004)

    Article  Google Scholar 

  36. Petrenko, A.: Fault model-driven test derivation from finite state models: Annotated bibliography. In: Cassez, F., Jard, C., Rozoy, B., Dermot, M. (eds.) MOVEP 2000. LNCS, vol. 2067, pp. 19–23. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  37. Eleftherakis, G., Kefalas, P., Sotiriadou, A.: Developing tools for formal methods. In: 9th Panhellenic Conference on Informatics, Thessaloniki, Greece, November 2003, pp. 625–639 (2003)

    Google Scholar 

  38. Pressman, R.: Software Engineering, a practitioner’s approach, 3rd edn. McGraw-Hill, London (1994)

    Google Scholar 

  39. Petrenko, A., Yevtushenko, N.: Testing from partial deterministic FSM specifications. IEEE Transactions on Computers 54(9), 1154–1165 (2005)

    Article  Google Scholar 

  40. Petrenko, A., Yevtushenko, N., von Bochmann, G.: Testing deterministic implementations from nondeterministic FSM specifications. In: Proc. of 9th International Workshop on Testing of Communicating Systems (IWTCS 1996), pp. 125–140 (1996)

    Google Scholar 

  41. Petrenko, A., Yevtushenko, N., von Bochmann, G., Dssouli, R.: Testing in context: framework and test derivation. Computer Communications 19, 1236–1249 (1996)

    Article  Google Scholar 

  42. Ramalingam, T., Das, A., Thulasiraman, K.: On testing and diagnosis of communication protocols based on the FSM model. Computer communications 18(5), 329–337 (1995)

    Article  Google Scholar 

  43. Stannett, M.: Complete behavioural testing (two extensions to state-machine testing. In: CONCUR 2002 Satellite Workshop on Formal Approaches To Testing (FATES), pp. 51–64 (2002)

    Google Scholar 

  44. Stannett, M.: The theory of X-machines. Technical Report CS-05-09, The University of Sheffield, UK (2006)

    Google Scholar 

  45. Tretmans, J.: Test generation with inputs, outputs and repetitive quiescence. Software – Concepts and Tools 17(3), 103–120 (1996)

    MATH  Google Scholar 

  46. Vanak, S.: Complete functional testing of hardware descriptions. PhD thesis, The University of Sheffield, UK (2002)

    Google Scholar 

  47. Vasilevskii, M.: Failure diagnosis of automata, vol. 4, pp. 653–665. Cybernetics, Plenum Publ. Corporation, New York (1973)

    Google Scholar 

  48. Wood, A.: Predicting software reliability. Computer 29(11), 69–77 (1996)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, The University of Sheffield Regent Court, 211 Portobello Street, Sheffield, S1 4DP, UK

    Kirill Bogdanov

Authors
  1. Kirill Bogdanov
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Robert M. Hierons Jonathan P. Bowen Mark Harman

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Bogdanov, K. (2008). Testing from X-Machine Specifications. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds) Formal Methods and Testing. Lecture Notes in Computer Science, vol 4949. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78917-8_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-78917-8_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-78916-1

  • Online ISBN: 978-3-540-78917-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation