The ingredients of typical model based development via refinement are re-examined, and some well known frameworks are reviewed in that light, drawing out commonalities and differen...
Abstract. In this paper we examine the difference between model checking high-level and low-level models. In particular, we compare the ProB model checker for the B-method and the ...
UML-B provides a graphical front end for Event-B. It adds support for class-oriented and state machine modelling. UML-B is similar to UML but has its own meta-model. UML-B provides...
Event-B is a formal modelling method which is claimed to be suitable for diverse modelling domains, such as reactive systems and sequential program development. This claim hinges o...
A Virtual Machine (VM) is a program running on a conventional microprocessor that emulates the binary instruction set, registers, and memory space of an idealized computing machine...
As systems become ever more complex, verification becomes more main stream. Event-B and Alloy are two formal specification languages based on fairly different methodologies. While...