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