Modelling a Multi-Agent System Relating to Liveness Properties in Event-B

Safety and liveness are properties of a formal model that ensure the correct and continuous progress of the model. The aim of this paper is to present a formal modelling and proof of correctness for a multi-agent system for requesting services, with respect to liveness properties fairness and starvation freedom. The model is specified and verified using the Event-B formalism and the Rodin platform an Eclipse plug-in meant to allow the writing and checking specification correctness. Event-B is a formal method based on first-order logic and set theory as an underlying mathematical notation used to model and reason about complex and discrete systems. One central mechanism of Event-B modelling is the concept of refinement that allows building a model in a step by step fashion, by adding more details to an initially abstract model, in order to reduce the level of abstraction, thus making it closer to reality. In our development we used refinement techniques, constructing an ordered sequence of embedded models, where each of them is a refinement of the one preceding it in the sequence.