Integration of ASM with Event-B RODIN

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.