Classical B is a state-based method developed by Abrial for specifying, designing and coding software systems. It is based on Zermelo^a€�?Fraenkel set theory with the axiom of choice. Sets are used for data modelling, generalised substitutions are used to describe state modifications, the refinement calculus is used to relate models at varying levels of abstraction, and there are a number of structuring mechanisms (machine, refinement and implementation) which are used in the organisation of a development. The first version of the B method is extensively described in The B Book 2. It is supported by the Atelier B tool 50 and by the B Toolkit 78.
%0 Book Section
%1 cansell_08_eventb
%A Cansell, Dominique
%A M'ery, Dominique
%D 2008
%J Logics of Specification Languages
%K 2008 _to_download_springer b
%P 47--152
%R http://dx.doi.org/10.1007/978-3-540-74107-7_3
%T The event-B Modelling Method: Concepts and Case Studies
%U http://dx.doi.org/10.1007/978-3-540-74107-7_3
%X Classical B is a state-based method developed by Abrial for specifying, designing and coding software systems. It is based on Zermelo^a€�?Fraenkel set theory with the axiom of choice. Sets are used for data modelling, generalised substitutions are used to describe state modifications, the refinement calculus is used to relate models at varying levels of abstraction, and there are a number of structuring mechanisms (machine, refinement and implementation) which are used in the organisation of a development. The first version of the B method is extensively described in The B Book 2. It is supported by the Atelier B tool 50 and by the B Toolkit 78.
@incollection{cansell_08_eventb,
abstract = {Classical B is a state-based method developed by Abrial for specifying, designing and coding software systems. It is based on Zermelo^{a}€�?Fraenkel set theory with the axiom of choice. Sets are used for data modelling, generalised substitutions are used to describe state modifications, the refinement calculus is used to relate models at varying levels of abstraction, and there are a number of structuring mechanisms (machine, refinement and implementation) which are used in the organisation of a development. The first version of the B method is extensively described in The B Book [2]. It is supported by the Atelier B tool [50] and by the B Toolkit [78].},
added-at = {2009-02-11T20:12:35.000+0100},
author = {Cansell, Dominique and M'{e}ry, Dominique},
biburl = {https://www.bibsonomy.org/bibtex/2ca2aadb1ff43647ce40d798fc976cc18/leonardo},
citeulike-article-id = {2075586},
doi = {http://dx.doi.org/10.1007/978-3-540-74107-7_3},
interhash = {86b4a3df02806863363e003d238a5832},
intrahash = {ca2aadb1ff43647ce40d798fc976cc18},
journal = {Logics of Specification Languages},
keywords = {2008 _to_download_springer b},
pages = {47--152},
posted-at = {2007-12-08 00:28:33},
priority = {2},
timestamp = {2009-02-11T20:12:35.000+0100},
title = {The event-B Modelling Method: Concepts and Case Studies},
url = {http://dx.doi.org/10.1007/978-3-540-74107-7_3},
year = 2008
}