Skip to main content
SpringerLink
Log in

Specification Coverage for Testing in Circus

  • Conference paper
Unifying Theories of Programming (UTP 2010)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6445))

Included in the following conference series:

Abstract

The Unifying Theories of Programming underpins the development of Circus, a state-rich process algebra for refinement. We have previously presented a theory of testing for Circus; it gives a symbolic characterisation of tests. Each symbolic test specifies constraints that capture the effect of the possibly nondeterministic state operations, and their interaction. This is a sound basis for testing techniques based on constraint solving for generation of concrete tests, but does not support well selection criteria based on the structure of the specification. We present here a labelled transition system that captures information about a Circus model and its structure. It is useful for testing techniques based on specification coverage. The soundness argument for the new transition system follows the UTP style, but relates the new transition relation to the Circus relational model and its operational semantics.

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. Bernot, G., Gaudel, M.-C., Marre, B.: Software testing based on formal specifications: a theory and a tool. Software Engineering Journal 6(6), 387–405 (1991)

    Article  Google Scholar 

  2. Bougé, L., Choquet, N., Fribourg, L., Gaudel, M.-C.: Test set generation from algebraic specifications using logic programming. Journal of Systems and Software 6(4), 343–360 (1986)

    Article  Google Scholar 

  3. Brinksma, E.: A theory for the derivation of tests. In: Protocol Specification, testing and Verification VIII, pp. 63–74. North-Holland, Amsterdam (1988)

    Google Scholar 

  4. Butterfield, A., Sherif, A., Woodcock, J.C.P.: Slotted Circus: A UTP-family of reactive theories. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 75–97. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  5. Cavalcanti, A.L.C., Gaudel, M.-C.: Testing for Refinement in CSP. In: Butler, M., Hinchey, M.G., Larrondo-Petrie, M.M. (eds.) ICFEM 2007. LNCS, vol. 4789, pp. 151–170. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  6. Cavalcanti, A.L.C., Gaudel, M.-C.: Testing for Refinement in Circus – Extended version. Technical report, University of York (2009), www-users.cs.york.ac.uk/~alcc/CG09.pdf

  7. Cavalcanti, A.L.C., Gaudel, M.-C.: A note on traces refinement and the conf relation in the Unifying Theories of Programming. In: Butterfield, A. (ed.) UTP 2008. LNCS, vol. 5713, pp. 42–61. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  8. Cavalcanti, A.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: Unifying Classes and Processes. Software and System Modelling 4(3), 277–296 (2005)

    Article  Google Scholar 

  9. Cavalcanti, A.L.C., Woodcock, J.C.P.: A Tutorial Introduction to CSP in Unifying Theories of Programming. In: Cavalcanti, A., Sampaio, A., Woodcock, J. (eds.) PSSE 2004. LNCS, vol. 3167, pp. 220–268. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  10. Chow, T.S.: Testing Software Design Modeled by Finite-State Machines. IEEE Transactions on Software Engineering SE-4(3), 178–187 (1978)

    Article  MATH  Google Scholar 

  11. 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)

    Chapter  Google Scholar 

  12. Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)

    MATH  Google Scholar 

  13. Frankl, P.G., Weyuker, E.J.: An applicable family of data-flow testing criteria. IEEE Transactions on Software Engineering 14(10), 1483–1498 (1988)

    Article  MathSciNet  Google Scholar 

  14. Gannon, J., McMullin, P., Hamlet, R.: Data abstraction implementation, specification and testing. ACM Transactions on Programming Languages and Systems 3(3), 211–223 (1981)

    Article  Google Scholar 

  15. Gaudel, M.-C.: 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)

    Chapter  Google Scholar 

  16. Harwood, W., Cavalcanti, A.L.C., Woodcock, J.C.P.: A Theory of Pointers for the UTP. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 141–155. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  17. Hierons, R.M., Kim, T.H., Ural, H.: On the testability of SDL specifications. Computer Networks 44(5), 681–700 (2004)

    Article  MATH  Google Scholar 

  18. Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)

    MATH  Google Scholar 

  19. Labbé, S., Gallois, J.-P.: Slicing communicating automata specifications: polynomial algorithms for model reduction. Formal Aspects of Computing 20(6), 563–595 (2008)

    Article  MATH  Google Scholar 

  20. Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines - A survey. Proceedings of the IEEE 84, 1090–1126 (1996)

    Article  Google Scholar 

  21. Millett, L.I., Teitelbaum, T.: Issues in slicing PROMELA and its applications to model checking, protocol understanding, and simulation. Software Tools for Technology Transfer 2(4), 343–349 (2000)

    Article  MATH  Google Scholar 

  22. Morgan, C.C.: Programming from Specifications, 2nd edn. Prentice-Hall, Englewood Cliffs (1994)

    MATH  Google Scholar 

  23. Oliveira, M.V.M.: Formal Derivation of State-Rich Reactive Programs Using Circus. PhD thesis, University of York (2006)

    Google Scholar 

  24. Oliveira, M.V.M., Cavalcanti, A.L.C., Woodcock, J.C.P.: Unifying Theories in ProofPowerZ. Formal Aspects of Computing (online first) (2007), doi:10.1007/s00165-007-0044-5

    Google Scholar 

  25. Oliveira, M.V.M., Cavalcanti, A.L.C., Woodcock, J.C.P.: A UTP Semantics for Circus. Formal Aspects of Computing 21(1-2), 3–32 (2009)

    Article  MATH  Google Scholar 

  26. Ranganath, V.P., Amtoft, T., Banerjee, A., Hatcliff, J., Dwyer, M.B.: A new foundation for control dependence and slicing for modern program structures. ACM Transactions on Programming Languages and Systems 29(5), 27 (2007)

    Article  MATH  Google Scholar 

  27. Robinson-Mallett, C., Hierons, R.M., Poore, J., Liggesmeyer, P.: Using communication coverage criteria and partial model generation to assist software integration testing. Software Quality Control 16(2), 185–211 (2008)

    Article  Google Scholar 

  28. Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall Series in Computer Science. Prentice-Hall, Englewood Cliffs (1998)

    Google Scholar 

  29. Santos, T.L.V.L., Cavalcanti, A.L.C., Sampaio, A.C.A.: Object Orientation in the UTP. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol. 4010, pp. 18–37. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  30. Schoot, H.V.D., Ural, H.: Data flow oriented test selection for LOTOS. Computer Networks and ISDN Systems 27(7) (1993)

    Google Scholar 

  31. Schoot, H.V.D., Ural, H.: Data flow analysis of system specifications in LOTOS. International Journal of Software Engineering and Knowledge Engineering 7, 43–68 (1997)

    Article  Google Scholar 

  32. Sherif, A., Cavalcanti, A.L.C., Jifeng, H., Sampaio, A.C.A.: A process algebraic framework for specification and validation of real-time systems. Formal Aspects of Computing 22(7), 153–191 (2009) (online first)

    MATH  Google Scholar 

  33. Tang, X., Woodcock, J.C.P.: Travelling Processes. In: Kozen, D., Shankland, C. (eds.) MPC 2004. LNCS, vol. 3125, pp. 381–399. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  34. Tripathy, P., Sarikaya, B.: Test Generation from LOTOS Specifications. IEEE Transactions on Computers 40(4), 543–552 (1991)

    Article  Google Scholar 

  35. Woodcock, J.C.P., Cavalcanti, A.L.C.: A Tutorial Introduction to Designs in Unifying Theories of Programming. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) IFM 2004. LNCS, vol. 2999, pp. 40–66. Springer, Heidelberg (2004); Invited tutorial

    Chapter  Google Scholar 

  36. Woodcock, J.C.P., Cavalcanti, A.L.C., Gaudel, M.-C., Freitas, L.J.S.: Operational Semantics for Circus. Formal Aspects of Computing (to appear)

    Google Scholar 

  37. Woodcock, J.C.P., Davies, J.: Using Z—Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of York, York, YO10 5DD, UK

    Ana Cavalcanti

  2. LRI, Université de Paris-Sud, France

    Marie-Claude Gaudel

  3. CNRS, Orsay, 91405, France

    Marie-Claude Gaudel

Authors
  1. Ana Cavalcanti
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marie-Claude Gaudel
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing, University of Teesside, Borough Road, TS1 3BA, Middlesbrough, UK

    Shengchao Qin

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cavalcanti, A., Gaudel, MC. (2010). Specification Coverage for Testing in Circus . In: Qin, S. (eds) Unifying Theories of Programming. UTP 2010. Lecture Notes in Computer Science, vol 6445. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16690-7_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-16690-7_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-16689-1

  • Online ISBN: 978-3-642-16690-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation