Abstract: Multi-agent systems (MAS) are increasingly used in critical applications. To ensure dependability of MAS, we need powerful development techniques that would allow us to master complexity inherent to MAS and formally verify correctness and safety of collaborative agent activities. In this paper we present a rigorous approach to development and verification of critical MAS in Event-B. We demonstrate how to formally specify complex agent interactions and verify their correctness and safety. We argue that refinement approach facilitates structuring complex requirements and formal reasoning about system-level properties. We illustrate our approach by a case study: formal development of a hospital MAS. Event-B; refinement; formal modelling; formal verification; multi-agent system; safety Mobile multi-agent systems (MAS) are complex decentralised distributed systems composed of agents asynchronously communicating with each other. Agents are computer programs acting autonomously on behalf of a person or an organisation, while coordinating their activities by communication (OMG Mobile Agents Facility, 1997). MAS are increasingly used in various critical applications such as factories, hospitals, rescue operations in disaster areas, etc. However, widespread use of MAS is currently hindered by the lack of methods for ensuring their dependability. In this paper we focus on studying complex agent interactions. In a critical MAS, incorrect execution of these activities might have devastating consequences. However, ensuring correctness of complex interactions is a challenging issue due to faults caused by agent disconnections, dynamic role allocation and autonomy of the agent behaviour. To address these challenges, we need the system-level modelling approaches that would support formal verification of correctness and facilitate discovery of restrictions that should be imposed on the system to guarantee its safety. In this paper we propose a refinement-based approach to developing critical MAS. Our formal modelling and verification framework is Event-B (Abrial, 2010). The main development technique of Event-B is refinement -a top-down approach to formal development of systems that are correct by construction. The system development starts from an abstract specification, which defines the main behaviour and properties of the system. The abstract specification is gradually transformed (refined) into a more concrete specification that is directly translatable into an implementation. Correctness of each refinement step is verified by proofs. These proofs establish system safety (via preservation of safety invariant properties expressed at different levels of abstraction) and liveness (via the 2 authors provable absence of undesirable system deadlocks). Transitivity of the refinement relation allows us to guarantee that the system implementation adheres to the abstract specifications. The Rodin platform (Rodin Platform, 2006) provides the developers with automated tool support for constructing and verifying system models in Event-B. The main novelty of our approach is in demonstrating how to gradually derive a system implementation that satisfies the desired safety properties. It is different from traditional approaches to verification of MAS that extract a model from a system implementation and verify the desired properties by state-exploration. Our approach is not only free of the state explosion problem but also allows the designers to discover restrictions that should be imposed on the system environment to guarantee system safety. The top-down development approach facilitates structuring of complex requirements and improves comprehensibility of formal models. We argue that the formal development in Event-B offers a useful technique for development and verification of complex critical MAS. The paper is structured as follows. In Section 2 we describe our formal modelling framework -Event-B. In Section 3 we define the main principles of formal reasoning about MAS and their properties. In Section 4 we present our case study -a hospital MAS. We show here how to abstractly model a MAS, introduce complex collaborative agent interactions by refinement, as well as verify safety properties. Moreover, we describe the last refinement step that models system decomposition, thus achieving derivation of a distributed implementation from a centralised specification. Finally, in Section 5 we overview the related work, discuss the achieved results and outline our future work. We start by briefly describing our formal development framework. The Event-B formalism is a variation of the B Method (Abrial, 2005), a state-based formal approach that promotes the correct-by-construction development paradigm and formal verification by theorem proving. Event-B has been specifically designed to model and reason about parallel, distributed and reactive systems. Currently Event-B is actively used within the FP7 ICT project Deploy to develop dependable systems from various domains (Deploy Project, 2008). In Event-B, a system specification (model) is defined using the notion of an abstract state machine (Abrial, 2010 ). An abstract state machine encapsulates the model state represented as a collection of model variables, and defines operations on this state, i.e., it describes the dynamic part (behaviour) of the modelled system. A machine may also have the accompanying component, called context, which contains the static part of the system. In particular, a context can include user-defined carrier sets, constants and their properties, which are given as a list of model axioms. A general form of Event-B models is given in Figure 1 . The machine is uniquely identified by its name M . The state variables, v, are declared in the Variables clause and initialised in the Init event. The variables are strongly typed by the constraining predicates I given in the Invariants clause.
Tarasyuk et al. REF proposed a formal approach for developing dynamic reconfigurable system in Event-B based on probabilistic verification technique to guarantee that system will discover possible reconfiguration strategy to meet service requirements despite failures of its vital components.
A refinement-based approach to developing critical multi-agent systems
IJCCBS
IJCCBS
Computer Science