Dependability-Explicit Engineering with Event-B: Overview of Recent Achievements <s> Goal-oriented refinement of reconfigurable systems <s> 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 development of hospital MAS by refinement in Event-B. We demonstrate that Event-B allows the developers to rigorously specify complex agent interactions and verify their correctness and safety. <s> BIB001 </s> Dependability-Explicit Engineering with Event-B: Overview of Recent Achievements <s> Goal-oriented refinement of reconfigurable systems <s> Multi-robotic systems are typical examples of complex multi-agent systems. The robots --- autonomic agents --- cooperate with each other in order to achieve the system goals. While designing multi-robotic systems, we should ensure that these goals remain achievable despite robot failures, i.e., guarantee system fault tolerance. However, designing the fault tolerance mechanisms for multi-agent systems is a notoriously difficult task. In this paper we describe a case study in formal development of a complex fault tolerant multi-robotic system. The system design relies on cooperative error recovery and dynamic reconfiguration. We demonstrate how to specify and verify essential properties of a fault tolerant multi-robotic system in Event-B and derive a detailed formal system specification by refinement. The main objective of the presented case study is to investigate suitability of a refinement approach for specifying a complex multi-agent system with co-operative error recovery. <s> BIB002 </s> Dependability-Explicit Engineering with Event-B: Overview of Recent Achievements <s> Goal-oriented refinement of reconfigurable systems <s> Goal-Oriented Development facilitates structuring complex requirements. To ensure resilience the designers should guarantee that the system achieves its goals despite changes, e.g., caused by failures of system components. In this paper we propose a formal goal-oriented approach to development of resilient MAS. We formalize the notion of goal and goal achievement in Event-B and propose the specification and refinement patterns that allow us to guarantee that the targeted goals are reached despite agent failures. We illustrate our approach by a case study --- development of an autonomous multi-robotic system. <s> BIB003 </s> Dependability-Explicit Engineering with Event-B: Overview of Recent Achievements <s> Goal-oriented refinement of reconfigurable systems <s> Ensuring fault tolerance of satellite systems is critical for achieving goals of the space mission. Since the use of redundancy is restricted by the size and the weight of the on-board equipments, the designers need to rely on dynamic reconfiguration in case of failures of some components. In this paper we propose a formal approach to development of dynamically reconfigurable systems in Event-B. Our approach allows us to build the system that can discover possible reconfiguration strategy and continue to provide its services despite failures of its vital components. We integrate probabilistic verification to evaluate reconfiguration alternatives. Our approach is illustrated by a case study from aerospace domain. <s> BIB004
In  BIB001 BIB002 , we have investigated the problem of ensuring safety and fault tolerance of mobile agent systems. The work has resulted in defining the modelling patterns to represent agent roles in dynamic scopes and deriving the logical conditions to ensure system dependability. In BIB003 , we have continued our study of multi-agent systems and have proposed a goal-oriented approach to development of multi-agent systems. It is currently recognized that the goal-oriented development facilitates design of complex dynamically adaptable systems. In goal-oriented development the system requirements are defined in terms of goals -the functional and non-functional objectives that a system should achieve. Often changes in system operational environment, e.g., caused by failures of agents -independent system components of various types -might hinder achieving the desired goals. In [ADA] we have proposed a formal development approach that ensures goal reachability "by construction". Essentially, our approach allows the developers to define system goals at different levels of abstraction and guarantee goal reachability despite agent failures. We have derived refinement patterns modelling the mechanisms for dynamic system reconfiguration by reallocating goals from failed agents to healthy ones and, per se, guarantee dependability. We believe that our approach offers a scalable technique for formal development of dynamically reconfigurable dependable systems. While refining a reconfigurable system, we had to assume that sufficient amount of agents would remain operational to achieve the desired goals. In BIB004 , we have demonstrated how to integrate probabilistic analysis to quantitatively assess the likelihood of goal reachability despite failures. The rigorous refinement process has allowed us to establish the precise relationships between component failures and goal reachability. We have assessed the derived reconfigurable system architecture to quantitatively verify that it achieves the desired reliability and performance objectives. This was accomplished by relying on the probabilistic extension of Event-B to verify reliability and performance properties using PRISM model checker  .