Evaluating Effectiveness of Rodin Animators For Consistency Checking

Abstract

Event-B is a formal language for modeling and reasoning about large reactive and distributed systems. Rodin is the tool that facilitates modeling in Event-B and supports the specification of machines and contexts, their refinements, and their consistency checking by automatically generating Proof Obligations. Rodin provides many different animators, such as AnimB and ProB, for consistency checking but all have their own limitations and liberations. The main focus of this project is to evaluate the effectiveness of these animators and improve the VTA framework by expanding its application to currently available animators. Several case studies will be explored including a Landing Gear System of an airplane. The capability of the animators to successfully execute the specifications will be checked along with a detailed investigation report on their failures and actions that can be taken to prevent such failures.