Common use of Modes Clause in Contracts

Modes. We have conducted a study of approaches to complex critical systems development, and the requirements documents within DEPLOY, and arrived at the following: • Separation of concerns is a major approach to tackle the complexity of the systems development. • A large amount of critical systems are developed using a notion of operation modes. • All critical systems involve operations with important aspects of human activity (e.g. lives, finance) hence critical. And all of them inevitably have faults due to changing environmental conditions, hardware failures etc. A high percentage of requirements to such systems (up to 40% according to our study within DEPLOY) include fault tolerance as a way to mitigate the consequences of errors. • Requirements evolve, including FT. There were neither mode nor fault tolerance viewpoints in the state of the art Event-B development. The UML-B approach of statecharts is closely related to modal views. However, the statecharts drive the development by generating Event-B models as opposed to the mode views which facilitate the development by leaving the Event-B modelling activity with the user. On the fault tolerance side, we are aware of the work on ProR framework for tracing requirements, and we plan to integrate the tracing framework with our modelling approach. The Mode/FT Views approach is to assist the main Event-B development by an additional set of abstractions and a toolset to facilitate modal and fault tolerance development. We were motivated by the following stimuli: • Facilitate the modal and fault tolerance development in Event-B with a comprehensible modelling approach. • Stimulate the consideration of fault tolerance at the very first phases of development. • Explicitly covering mode and fault tolerance concerns, we wanted to improve the requirement traceability and fulfilment. • Help make planning decisions. Focusing the developer attention on specific aspects of development leads to better understanding of the problem and planning of the solution. • Provide consistent way of stepwise development of mode and FT aspects by a notion of views refinement.