Dependability-Explicit Engineering with Event-B: Overview of Recent Achievements <s> Formal development of fault tolerant mode-rich systems <s> One of the guarantees that the designers of on-board satellite systems need to provide, so as to ensure their dependability, is that the mode transition scheme is implemented correctly, i.e. that the states of system components are consistent with the global system mode. There is still, however, a lack of scalable approaches to developing and verifying systems with complex mode transitions. This paper presents an approach to the formal development of mode-rich systems by refinement in Event-B. We formalise the concepts of modes and mode transitions as well as deriving specification and refinement patterns which support correct-by-construction system development. The proposed approach is validated by a formal development of the Attitude and Orbit Control System (AOCS) undertaken within the ICT DEPLOY project. The experience gained in the course of developing such a complex industrial system as AOCS, shows that Event-B refinement provides the engineers with a scalable formal technique. Moreover, the case study has demonstrated that Event-B can facilitate formal development of mode-rich systems and, in particular, proof-based verification of their mode consistency. <s> BIB001 </s> Dependability-Explicit Engineering with Event-B: Overview of Recent Achievements <s> Formal development of fault tolerant mode-rich systems <s> To ensure dependability of on-board satellite systems, the designers should, in particular, guarantee correct implementation of the mode transition scheme, i.e., ensure that the states of the system components are consistent with the global system mode. However, there is still a lack of scalable approaches to formal verification of correctness of complex mode transitions. In this paper we present a formal development of an Attitude and Orbit Control System (AOCS) undertaken within the ICT DEPLOY project. AOCS is a complex mode-rich system, which has an intricate mode-transition scheme. We show that refinement in Event B provides the engineers with a scalable formal technique that enables both development of mode-rich systems and proof-based verification of their mode consistency. <s> BIB002 </s> Dependability-Explicit Engineering with Event-B: Overview of Recent Achievements <s> Formal development of fault tolerant mode-rich systems <s> Space satellites are examples of complex embedded systems. Dynamic behaviour of such systems is typically described in terms of operational modes that correspond to the different stages of a mission and states of the components. Components are susceptible to various faults that complicate the mode transition scheme. Yet the success of a mission depends on the correct implementation of mode changes. In this paper we propose a formal approach that ensures consistency of mode changes while developing a system architecture by refinement. The approach relies on recursive application of modelling and refinement patterns that enforce correctness while implementing the mode transition scheme. The proposed approach is exemplified by the development of an Attitude and Orbit Control System undertaken within the ICT DEPLOY project. <s> BIB003 </s> Dependability-Explicit Engineering with Event-B: Overview of Recent Achievements <s> Formal development of fault tolerant mode-rich systems <s> Modes are widely used to structure the behaviour of control systems. For many such systems, derivation and verification of a mode logic is challenging due to a large number of modes and complex mode transitions. In this paper we propose an approach to deriving, formalising and verifying consistency of a mode logic for fault tolerant control systems. We demonstrate how to use Failure Modes and Effects Analysis (FMEA) to systematically derive the fault tolerance part of the mode logic. To tackle the problem of mode consistency, we propose a formalisation of the mode logic and mode consistency conditions for layered systems with reconfigurable components. We use our formalisation to develop and verify a mode-rich system by refinement in Event-B. <s> BIB004
A widely used mechanism for achieving fault tolerance is based on the notion of modes. In our work BIB002 BIB003 BIB001 , we have proposed an approach to formal development of fault tolerant mode-rich systems. Such systems achieve fault tolerance by rollbacking to specific degraded modes. The proposed formal development process allows the designers to develop a system in a layered fashion. Essentially, it consists of a number of steps gradually unfolding system architectural layers by refinement. Moreover, we prove the consistency between mode transitions on adjacent architectural layers, which significantly improves scalability of verification. It has been noted that testing and model checking of the systems with complex mode transition schemes suffers from poor scalability. We have overcame this problem by relying on incremental verification of global mode consistency properties by proof and hence achieved a good scalability. In our approach to modelling mode-rich systems BIB002 BIB003 BIB001 , we have focused on verification of consistency of a predefined mode logic. In BIB004 , we have proposed to conduct Failure Modes and Effects Analysis (FMEA) of each operational mode to identify mode transitions required to implement fault tolerance. Fault tolerance is achieved by two different means -transitions to a more degraded mode and dynamic reconfiguration using redundant components. Furthermore, we have investigated a complex interplay between the states of components during reconfiguration and the system modes.