Advertisement

Extraction of Abstraction Invariants for Data Refinement

  • Marielle Doche
  • Andrew Gravell
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2272)

Abstract

In this paper, we describe an approach to generating abstraction invariants for data refinement from specifications mixing B and CSP notations. A model-checker can be used to check automatically refinement of the CSP parts. However, we need to translate the CSP into B in order to verify data refinement of the whole specification. The Csp2B tool generates the B specification automatically from the CSP parts. Our proposal is to generate in addition the abstraction invariants, by analysing the labelled transition systems provided by a model-checker. The approach is illustrated with a case study in which a simple distributed information system is specified and two refinements are given, both of which have been fully verified using the proposed combination of model-checking with theorem proving (both automatic and interactive).

Keywords

Formal specification CSP failure refinement data refinement distributed system 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [Abr96]
    J-R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996.Google Scholar
  2. [AL91]
    M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2), May 1991.Google Scholar
  3. [B-C99]
    B-Core (UK) Limited, Oxon, UK. B-Toolkit, On-line manual., 1999. Available at http://www.b-core.com/ONLINEDOC/Contents.html.
  4. [But97]
    M. J. Butler. An approach to the design of distributed systems with B AMN. In J. Bowen, M. Hinchey, and D. Till, editors, Proc. 10th Int. Conf. of Z Users: The Z Formal Specification Notation (ZUM), LNCS 1212, pages 223–241, Reading, UK, April 1997. Springer-Verlag, Berlin. Available at http://www.dsse.ecs.soton.ac.uk/.Google Scholar
  5. [But99]
    M. J. Butler. csp2B: A practical approach to combining CSP and B. In J. M. Wing, J. Woodcock, and J. Davies, editors, Proc. FM’99: World Congress on Formal Methods, LNCS 1708, pages 490–508. Springer-Verlag, Berlin, September 1999. Available at http://www.dsse.ecs.soton.ac.uk/.Google Scholar
  6. [DS00]
    J. Derrick and G. Smith. Structural refinement in object-z / csp. In IFM’2000 (Integrated Formal Methods), volume 1945 of LNCS. Springer-Verlag, 2000. Available at http://www.cs.ukc.ac.uk/research/tcs/index.html.CrossRefGoogle Scholar
  7. [For97]
    Formal Systems (Europe) Ltd. Failures-Divergence Refinement-FDR2 user manual, Octobre 1997. Available at www.formal.demon.co.uk/fdr2manual/index.html.
  8. [FW99]
    C. Fischer and H. Wehrheim. Model-checking CSP-OZ specifications with FDR. In First international Conference on Integrated Formal Methods (IFM99), pages 315–334. Springer-Verlag, 1999. Available at http://semantik.Informatik.Uni-Oldenburg.DE/persons/clemens.ficher/.
  9. [HBC+99]
    P. Hartel, M. Butler, A. Currie, P. Henderson, M. Leuschel, A. Martin, A. Smith, U. Ultes-Nitsche, and B. Walters. Questions and answers about ten formal methods. In S. Gnesi and D. Latella, editors, Proc. 4th Int. Workshop on Formal Methods for Industrial Critical Systems, volume II, pages 179–203, Trento, Italy, July 1999. ERCIM, STAR/CNR, Pisa, Italy. Available at http://www.dsse.ecs.soton.ac.uk/.
  10. [Hoa85]
    C.A.R Hoare. Communicating Sequential Processes. Prentice Hall, 1985.Google Scholar
  11. [MC99]
    I. MacColl and D. Carrington. Specifying interactive systems in Object-Z and CSP. In First international Conference on Integrated Formal Methods (IFM99). Springer-Verlag, 1999. Available at http://archive.csse.uq.edu.au/ ianm/.
  12. [Mor90]
    C.C. Morgan. Of wp and CSP. In W.H.J. Feijen, A.J.M. van Gasteren, D. Gries, and J. Misra, editors, Beauty is our business: a birthday salute to Edsger W. Dijkstra. Springer Verlag, 1990.Google Scholar
  13. [MS98]
    A. Mota and A. Sampaio. Model-checking CSP-Z. In Fundamental Approach of Software Engineering (FASE98), number 1382 in LNCS, pages 205–220. Springer Verlag, 1998. Available at http://www.di.ufpe.br/ acm/.CrossRefGoogle Scholar
  14. [Ros97]
    A.W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 1997.Google Scholar
  15. [Spi92]
    J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall International Series in Computer Science, 2nd edition, 1992.Google Scholar
  16. [WM90]
    J.C.P. Woodcock and C.C. Morgan. Refinement of state-based concurrent systems. In D. Bjorner, C.A.R. Hoare, and H. Langmaack, editors, VDM’90, volume 428 of LNCS. Springer-Verlag, 1990. Available at http://www.iro.umontreal.ca/labs/teleinfo/PubListIndex.html.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Marielle Doche
    • 1
  • Andrew Gravell
    • 1
  1. 1.Department of Electronics and Computer ScienceUniversity of SouthamptonHighfield SouthamptonUK

Personalised recommendations