Reconciling Axiomatic and Model-Based Specifications Using the B Method

Abstract

The worlds of model-based and axiomatic specification are frequently regarded as separate. The formal specification notations of Z and B (the B Method) are usually employed for mathematical modelling. On the other hand, it could be desirable to base some part of a specification on a set of axioms. The axiomatic specification provides an additional capability for validating a specification, while reconciling the axiomatic specification with a model-based specification would allow the development of an implementation to be based on the model-based specification. This paper develops a framework that uses the B Method and an associated toolkit to provide a formal reconciliation between an axiomatic specification and a model-based specification. The framework provides a strategy for proving a refinement relation between two (specification) machines.