Formal development and quantitative verification of dependable systems

Abstract

Modern software-intensive systems are becoming increasingly complex. Yet we are observing the pervasive use of software in such critical infrastructures as transportation systems, healthcare, telecommunication, energy produc- tion, etc. Consequently, we tend to place increasing reliance on computer- based systems and the software that they are running. The degree of reliance that we can justifiably place on a system is expressed by the notion of de- pendability. Designing highly-dependable systems is a notoriously difficult task. It requires rigorous mathematical methods to prevent design errors and guar- antee the correct and predictable system behaviour. However, fault pre- vention via rigorous engineering still cannot ensure avoidance of all faults. Hence we need powerful mechanisms for tolerating faults, i.e., the solutions that allow the system to confine the damage caused by fault occurrence and guarantee high reliability and safety. Traditionally, such dependabil- ity attributes are assessed probabilistically. However, the current software development methods suffer from discontinuity between modelling the func- tional system behaviour and probabilistic dependability evaluation. To ad- dress these issues, in the thesis we aim at establishing foundations for a rigorous dependability-explicit development process. In particular, we pro- pose a semantic extension of Event-B – an automated state-based formal development framework – with a possibility of quantitative (probabilistic) reasoning. Event-B and its associated development technique – refinement – provide the designers with a powerful framework for correct-by-construction systems development. Via abstract modelling, proofs and decomposition it allows the designers to derive robust system architectures, ensure pre- dictable system behaviour and guarantee preservation of important system properties. We argue that the rigorous refinement-based approach to system devel- opment augmented with probabilistic analysis of dependability significantly facilitates development of complex software systems. Indeed, the proposed probabilistic extension of Event-B allows the designers to quantitatively as- sess the effect of different fault tolerance mechanisms and architectural solu- tions on system dependability. Moreover, it enables the stochastic reasoning about the impact of component failures and repairs on system reliability and safety from the early design stages. The proposed enhanced version of the standard Event-B refinement allows the designers to ensure that the developed system is not only correct-by-construction but also dependable- by-construction, i.e., it guarantees that refinement improves (or at least preserves) the probabilistic measure of system dependability. The proposed extension has been validated by a number of case stud- ies from a variety of application domains, including service-oriented sys- tems, aerospace, railways and communicating systems. We believe that the research presented in the thesis contributes to creating an integrated dependability-explicit engineering approach that facilitates rigorous devel- opment of complex computer-based systems.