Abstract:
This thesis is related to the integration of diverse formal veri cation tools
to harness their capabilities for better modeling and veri cation of complex
systems. In this e ort we worked on integrating Abstract State Machines
(ASMs) with Event-B using the RODIN platform.
Event-B is a formal veri cation tool that is used for real-time system-level
modeling and analysis. Event-B is primarily based on the B Method, which is
a formal method for the development of program code from a speci cation in
the Abstract Machine Notation. Event-B uses sets and rst-order predicate
logic as its foundations. It allows di erent abstraction levels to be shown
using re nements. Event-B is supported by the RODIN platform that uses
the Eclipse IDE. ASMs are very easy to develop and manipulate but their
veri cation is an issue. The tool set is not that rich in veri cation. Whereas
RODIN toolset is very rich in Veri cation and Validation of the requirements.
In particular, in the thesis, we de ne Event-B and ASMs and the tech-
nique we devised to perform their translation (ASM to Event-B). Moreover
there is an architectural and visual design of the tool-set that we propose to
develop for this translation.
