[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

Model checking of state-rich formalism by linking to \(CSP\,\Vert \,B\)

  • Regular Paper
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

Since state-rich formalism

is a combination of Z, CSP, refinement calculus and Dijkstra’s guarded commands, its model checking is intrinsically more complicated and difficult than that of individual state-based languages or process algebras. Current solutions translate executable constructs of

programs to Java with JCSP, or translate them to CSP processes. Data aspects of

programs are expressed in the Java programming language or as CSP processes. Both of them have disadvantages. This work presents a new approach to model-checking

by linking it to \(CSP \parallel B\); then we utilise ProB to model-check and animate the \(CSP \parallel B\) program. The most significant advantage of this approach is the direct mapping of the state part in

to Z and finally to B, which maintains the high-level abstraction of data specification. In addition, introduction of deadlock, invariant violation checking, LTL formula checking and animation is another key advantage. We present our approach, a link definition for a subset of

constructs, as well as a popular case study (reactive buffer) to show the practical usability of our work. We conclude with a discussion of related work, advantages and potential limitations of our approach and future work.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13
Fig. 14
Fig. 15
Fig. 16

Similar content being viewed by others

References

  1. FDR2: a refinement checker for establishing properties of models expressed in CSP. www.fsel.com/software.html

  2. SICStus prolog manual (arithmetic expressions). https://sicstus.sics.se/sicstus/docs/latest4/html/sicstus.html/ref_002dari_002daex.html#ref_002dari_002daex

  3. The ProB animator and model checker. http://www.stups.uni-duesseldorf.de/ProB/index.php5/Main_Page

  4. ISO/IEC: Information technology-Z formal specification notation-syntax, type system and semantics (2002). http://standards.iso.org/ittf/PubliclyAvailableStandards/c021573_ISO_IEC_13568_2002(E).zip

  5. Abrial, J.R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (2005)

    MATH  Google Scholar 

  6. Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)

    Book  MATH  Google Scholar 

  7. Beg, A., Butterfield, A.: Linking a state-rich process algebra to a state-free algebra to verify software/hardware implementation. In: Proceedings of the 8th International Conference on Frontiers of Information Technology (FIT ’10), pp. 47:1–47:5. ACM, New York (2010)

  8. Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Inf. Control 60(1–3), 109–137 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  9. Butler, M., Leuschel, M.: Combining CSP and B for specification and property verification. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds.) FM 2005: Formal Methods. Lecture Notes in Computer Science, vol. 3582, pp. 221–236. Springer, Berlin, Heidelberg (2005)

    Chapter  Google Scholar 

  10. Carlsson, M.: Sicstus PROLOG user’s manual 4. Swedish Institute of Computer Science (2015). ISBN: 9783735737441. https://sicstus.sics.se/sicstus/docs/latest4/pdf/sicstus.pdf

  11. Carrington, D.A., Duke, D.J., Duke, R., King, P., Rose, G.A., Smith, G.: Object-Z: an object-oriented extension to Z. In: Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE ’89), pp. 281–296. North-Holland Publishing Co., Amsterdam (1990)

  12. Cavalcanti, A., Sampaio, A., Woodcock, J.: A refinement strategy for Circus. Form. Asp. Comput. 15(2–3), 146–181 (2003)

    Article  MATH  Google Scholar 

  13. Cavalcanti, A., Woodcock, J.: A tutorial introduction to CSP in unifying theories of programming. In: Cavalcanti, A., Sampaio, A., Woodcock, J. (eds.) Refinement Techniques in Software Engineering. Lecture Notes in Computer Science, vol. 3167, pp. 220–268. Springer, Berlin, Heidelberg (2006)

    Chapter  Google Scholar 

  14. Clarke Jr, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  15. Clearsy: B language reference manual (version 1.8.6). http://www.atelierb.eu/ressources/manrefb1.8.6.uk.pdf

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

    MATH  Google Scholar 

  17. Eclipse: Eclipse public license–v 1.0. http://www.eclipse.org/org/documents/epl-v10.html

  18. Fischer, C.: CSP-OZ: a combination of object-Z and CSP (1997)

  19. Fischer, C.: How to combine Z with process algebra. In: ZUM, pp. 5-23 (1998)

  20. Formal systems (Europe) Ltd: FDR2 user manual, fdr 2.94 edn (2012)

  21. Freitas, L.: Model checking Circus. Ph.D. thesis (2005)

  22. Freitas, A., Cavalcanti, A.: Automatic translation from Circus to Java. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006: Formal Methods. Lecture Notes in Computer Science, vol. 4085, pp. 115–130. Springer, Berlin, Heidelberg (2006)

    Chapter  Google Scholar 

  23. Galloway, A., Stoddart, B.: An operational semantics for ZCCS. In: Proceedings of the 1st International Conference on Formal Engineering Methods (ICFEM ’97). IEEE Computer Society, Washington, DC (1997). ISBN: 0-8186-8002-4

  24. Hoare, C., He, J.: Unifying Theories of Programming, vol. 14. Prentice Hall, Englewood Cliffs (1998)

  25. Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)

    MATH  Google Scholar 

  26. Jones, C.B.: Systematic Software Development using VDM, 2nd edn. Prentice Hall, Englewood Cliffs. Prentice Hall International Series in Computer Science (1991)

  27. Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, Boston (2002)

  28. Lazic, R.: A semantic study of data independence with application to model checking. Ph.D. thesis (1999). http://www.dcs.warwick.ac.uk/~lazic/thes_corr.ps.gz

  29. Leijen, D.: Division and modulus for computer scientists (2001). http://research.microsoft.com/pubs/151917/divmodnote.pdf

  30. Leuschel, M., Butler, M.J.: Automatic refinement checking for B. In: ICFEM, pp. 345-359 (2005)

  31. Marcel Oliveira Augusto Sampaio, P.A.R.R.A.C.J.W.: Compositional analysis and design of CML models. COMPASS deliverable D24.1 (2013)

  32. Milner, R.: A Calculus of Communicating Systems. Lecture Notes in Computer Science, vol. 92. Springer, Berlin (1980)

  33. Morgan, C.C.: Programming from Specifications. Prentice Hall International Series in Computer Science 2nd edn. Prentice Hall, Englewood Cliffs (1994)

  34. Mota, A., Sampaio, A.: Model-Checking CSP-Z. In: FASE, pp. 205–220 (1998)

  35. Nogueira, S., Sampaio, A., Mota, A.: Test generation from state based use case models. Form. Asp. Comput. 1-50 (2012). doi:10.1007/s00165-012-0258-z

  36. Oliveira, M.V.: Formal derivation of state-rich reactive programs using Circus. Ph.D. thesis, University of York (2005)

  37. Oliveira, M., Cavalcanti, A., Woodcock, J.: Formal development of industrial-scale systems in Circus. ISSE 1(2), 125–146 (2005)

    Google Scholar 

  38. Oliveira, M., Cavalcanti, A., Woodcock, J.: A denotational semantics for Circus. Electr. Notes Theor. Comput. Sci. 187, 107–123 (2007)

    Article  Google Scholar 

  39. Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for Circus. Form. Asp. Comput. 21(1–2), 3–32 (2009)

    Article  MATH  Google Scholar 

  40. Oliveira, M., Sampaio, A., Conserva Filho, M.: Model-checking Circus state-rich specifications. In: E. Albert, E. Sekerinski (eds.) Integrated Formal Methods, Lecture Notes in Computer Science, pp. 39-54. Springer International Publishing, Berlin (2014). doi:10.1007/978-3-319-10181-1_3

  41. Plagge, D., Leuschel, M.: Validating Z specifications using the ProB animator and model checker. In: J. Davies, J. Gibbons (eds.) Integrated Formal Methods, Lecture Notes in Computer Science, vol. 4591, pp. 480-500. Springer, Berlin (2007). doi:10.1007/978-3-540-73210-5_25

  42. Roscoe, A.: Understanding Concurrent Systems, 1st edn. Springer, New York (2010)

    Book  MATH  Google Scholar 

  43. Roscoe, A.W., Hoare, C.A.R., Bird, R.: The Theory and Practice of Concurrency. Prentice Hall PTR, Upper Saddle River, NJ, USA (1997)

    Google Scholar 

  44. Roscoe, A.W., Woodcock, J., Wulf, L.: Non-interference through determinism. J. Comput. Secur. 4(1), 27–54 (1996)

    Article  Google Scholar 

  45. Scattergood, B.: The semantics and implementation of machine-readable CSP. Ph.D. thesis, University of Oxford (1998)

  46. Schneider, S., Treharne, H.: CSP theorems for communicating B machines. Form. Asp. Comput. 17(4), 390–422 (2005)

    Article  MATH  Google Scholar 

  47. Spivey, J.M.: Z Notation: A Reference Manual: Prentice Hall International Series in Computer Science, 2nd edn. Prentice Hall, Englewood Cliffs (1992)

  48. Welch, P.H.: Process oriented design for Java: concurrency for all. In: PDPTA, vol. 1, pp. 51–57. CSREA Press (2000)

  49. Woodcock, J., Cavalcanti, A.: The semantics of Circus. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002: Formal Specification and Development in Z and B. Lecture Notes in Computer Science, vol. 2272, pp. 184–203. Springer, Berlin, Heidelberg (2002)

  50. Woodcock, J., Cavalcanti, A.: A tutorial introduction to designs in unifying theories of programming. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) Integrated Formal Methods. Lecture Notes in Computer Science, vol. 2999, pp. 40–66. Springer, Berlin, Heidelberg (2004)

    Chapter  Google Scholar 

  51. Woodcock, J., Cavalcanti, A., Freitas, L.: Operational semantics for model checking Circus. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds.) FM 2005: Formal Methods. Lecture Notes in Computer Science, vol. 3582, pp. 237–252. Springer, Berlin, Heidelberg (2005)

    Chapter  Google Scholar 

  52. Woodcock, J., Cavalcanti, A., Gaudel, M.C., Freitas, L.: Operational semantics for Circus. Formal aspects of computing (2007). https://www.cs.york.ac.uk/ftpdir/pub/leo/utp/journal-pub/circus-operational-semantics.pdf

Download references

Acknowledgments

We thank Leo Freitas and Andrew Butterfield for discussions about the link approach, CZT as well as the insights of difficulties.

Author information

Authors and Affiliations

  1. Department of Computer Science, University of York, York, UK

    Kangfeng Ye & Jim Woodcock

Authors
  1. Kangfeng Ye
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jim Woodcock
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Kangfeng Ye.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Ye, K., Woodcock, J. Model checking of state-rich formalism by linking to \(CSP\,\Vert \,B\) . Int J Softw Tools Technol Transfer 19, 73–96 (2017). https://doi.org/10.1007/s10009-015-0402-1

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-015-0402-1

Keywords

Search

Navigation