You are here: TUCS > EDUCATION > TUCS Graduate Programmes > Students > Anton Tarasyuk
Dr. Anton Tarasyuk
Date of doctoral defense: 28.1.2013
TUCS Department for the doctoral studies: Åbo Akademi University, Department of Information Technologies
Admitted to TUCS GP on 15.9.2009
Graduate project title:
Formal Development and Quantitative Verification of Dependable Systems
Graduate project 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 production, 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 dependability.
Designing highly-dependable systems is a notoriously difficult task. It requires rigorous mathematical methods to prevent design errors and guarantee the correct and predictable system behaviour. However, fault prevention 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 dependability attributes are assessed probabilistically. However, the current software development methods suffer from discontinuity between modelling the functional system behaviour and probabilistic dependability evaluation. To address these issues, in the thesis we aim at establishing foundations for a rigorous dependability-explicit development process. In particular, we propose 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 predictable system behaviour and guarantee preservation of important system properties.
We argue that the rigorous refinement-based approach to system development 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 assess the effect of different fault tolerance mechanisms and architectural solutions 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 studies from a variety of application domains, including service-oriented systems, 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 development of complex computer-based systems.
Former supervisors:
Kaisa Sere (Åbo Akademi University, Department of Information Technologies)
Elena Troubitsyna (Åbo Akademi University, Department of Information Technologies)
Latest publications:
Click here to see the full list of publications from the TUCS Publication Database