You are here: Home Tutorials Tutorial 4
Tutorial 4 PDF Print E-mail

HALF-DAY TUTORIAL

 

Tutorial 4

Tutorial 4. September 22, 2011,  h. 09:00-13:00, room B, ground floor

Elena Troubitsyna1, Alexei Iliasov2 and Linas Laibinis3,
1Academy of Finland, Finland; 2Newcastle University, Newcastle-upon-Tyne, UK; 3Åbo Akademi University, Finland

Title: Correct-by-Construction Development of Dependable Systems

Abstract: The degree of reliance, which we can place on a computer-based system, is expressed by the notion of dependability. Dependability is a multi-facet system characteristic that includes such attributes as safety, reliability, availability etc. There are two complementary principles to achieve system dependability: fault prevention and fault tolerance. The aim of fault prevention is to ensure that faults are not present in the operational system, e.g., by applying formal development techniques for establishing system correctness. However, fault prevention cannot be applied to uncontrollable fault sources such as, e.g., hardware faults. Furthermore, attempts to eliminate all design faults are often impractical. Hence, to achieve dependability we should combine the techniques for fault prevention and fault tolerance. It is well-known that dependability-explicit development process allows us to construct systems that are more robust, well-structured and have a higher degree of dependability. Our tutorial aims at providing researchers and industry practitioners with a systematic introduction into the formal dependability-explicit development process. The tutorial will give a comprehensive introduction into formal correct-by-construction development paradigm as well as overview the advanced topics in formal modelling and verification of dependable system.

We will describe principles of system modelling and development by refinement in Event B. The Event B framework [2] has been successfully used in industrial setting and has a mature automatic tool support – Rodin platform [3]. A succession of several EU projects has allowed us to gain a rich experience in Event-B modelling of dependable systems from various industrial domains. In the tutorial we will focus on modelling and verification of system safety and fault tolerance and overview our experience in these areas.

The tutorial aims at demonstrating that correct-by-construction development in Even-B offers a scalable highly-automated rigorous technique to system development and verification. It allows the designers to derive a robust system architecture, formally verify safety and efficiently structure fault tolerance mechanisms.

References

1. J.-R.Abrial. The B-book: assigning programs to meanings. Cambridge University Press, 1996.

2. J.-R. Abrial. Modelling in Event B. Cambridge University Press, 2010.

3. Rodin platform. Available from http://www.event-b.org/

Instructors Bio:

Alexei Iliasov is a Researcher Associate at the Faculty of Computing Science of Newcastle University, Newcastle-upon-Tyne, UK. He got his PhD in Computer Science in 2008 in the area of modelling artefacts reuse in formal developments. His research interests include agent systems, formal methods for software engineering and tools and environments supporting modelling and proof.

Linas Laibinis is a Senior Researcher at the Department of Information Technologies of Åbo Akademi University, Finland. He got his PhD in Computer Science in 2000 on mechanised formal reasoning about computer programs. His research interests include interactive environments for proof and program construction, as well as application of formal methods to modelling and development of fault tolerant and distributed software systems.

Elena Troubitsyna is an Academy Research Fellow at the Academy of Finland and Adj.Professor at the Department of IT at Abo Akademi University. She got her PhD in Computer Science in 2000 on design methods for dependable systems. Her research interests include application of formal and structured methods to development of dependable complex systems. She is a leader of several national projects in the area of dependability and formal methods. She has also served in numerous programme committees of international conferences. Elena is a PC chair of SERENE 2011 -- International Workshop on Software Engineering for Resilient Systems.

Expected Duration: 4 hours