FOUNDATIONS OF THE B METHOD
Dominique Cansell, Dominique Méry
2003
Computing and Informatics, Vol. 22, 2003, 1–31
Abstract.
B is a method for specifying, designing and coding software systems. It is
based on Zermelo-Fraenkel set theory with the axiom of choice, the concept of
generalized substitution and on structuring mechanisms (machine,refinement,
implementation). The concept of refinement is the key notion for developing B
models of (software) systems in an incremental way. B models are accompanied
by mathematical proofs that justify them. Proofs of B models convince the
user (designer or specifier) that the (software) system is effectively correct. We
provide a survey of the underlying logic of the B method and the semantic
concepts related to the B method; we detail the B development process partially
supported by the mechanical engine of the prover.
Keywords: Events, Actions, Systems, Refinement, Proof, Validation, Formal
Method.
Comments
Post a Comment