In this paper we propose to combine two software verification approaches, theorem proving and model checking. We focus on the B-method and a theorem proving tool associated with it, and the Alloy specification notation and its model checker “Alloy Constraint Analyser”. We consider how software development in B can be assisted using Alloy and how Alloy can be used for verifying refinement of abstract specifications. We demonstrate our approach with an example.
CITATION STYLE
Mikhailov, L., & Butler, M. (2002). An approach to combining B and alloy. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2272, pp. 140–161). Springer Verlag. https://doi.org/10.1007/3-540-45648-1_8
Mendeley helps you to discover research relevant for your work.