Extraction of Abstraction Invariants for Data Refinement
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).
KeywordsFormal specification CSP failure refinement B data refinement distributed system
Unable to display preview. Download preview PDF.
- [Abr96]J-R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996.Google Scholar
- [AL91]M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2), May 1991.Google Scholar
- [B-C99]B-Core (UK) Limited, Oxon, UK. B-Toolkit, On-line manual., 1999. Available at http://www.b-core.com/ONLINEDOC/Contents.html.
- [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
- [For97]Formal Systems (Europe) Ltd. Failures-Divergence Refinement-FDR2 user manual, Octobre 1997. Available at www.formal.demon.co.uk/fdr2manual/index.html.
- [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/.
- [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/.
- [Hoa85]C.A.R Hoare. Communicating Sequential Processes. Prentice Hall, 1985.Google Scholar
- [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/.
- [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
- [Ros97]A.W. Roscoe. The Theory and Practice of Concurrency. Prentice-Hall, 1997.Google Scholar
- [Spi92]J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall International Series in Computer Science, 2nd edition, 1992.Google Scholar
- [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