Correct-by-Construction Development of Dependable Systems

Presenters:

Alexei Iliasov (Senior RA, Newcastle University, UK)
Linas Laibinis (Senior RA, Aabo Akademi University, Finland)
Elena Troubitsyna (Prof, Aabo Akademi University, Finland)
Alexander Romanovsky (Prof, Newcastle University, UK)

Contacts:

[email protected]
[email protected]

Abstract

The degree of reliance that we can place on a computer‐based system is expressed by the notion of dependability. Dependability is a multi‐faceted system characteristic that includes such attributes as safety, reliability, availability, and so forth. There are two complementary principles necessary 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 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 a dependability‐explicit development process allows us to construct systems that are more robust and well‐structured with a higher degree of dependability. Our tutorial aims to provide researchers and industry practitioners with a systematic introduction into the formal dependability-­explicit development process. The tutorial will give a comprehensive introduction of the formal correct-­by-­construction development paradigm as well as overview the advanced topics in formal modeling and verification of dependable system.

We will describe principles of system modeling and development by refinement in Event‐B. The Event-­B framework has been successfully used in industrial setting and has a mature automatic tool support – the Rodin platform (http://www.event‐b.org/). A succession of several EU projects has allowed us to gain a rich experience in Event-­B modeling of dependable systems from various industrial domains. In the tutorial, we will focus on modeling 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 Event-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.

This will be a hand-on tutorial in which participants will be able to gain experience in using the method and the tool. Participants can bring their laptops, and we will help them to install the tool before the tutorial. A dedicated web site will be setup in advance to provide the participants with preparatory information (tools, documentation, examples). The tutorial will start with a general introduction of the principles of developing dependable systems, the Event-B method, and the Rodin tool. In the second and third parts of the tutorial, we will work together on developing several simple but nontrivial systems that have characteristics of the real applications from several application domains. The tutorial will conclude with a description of the Event-B ecosystem.

Tutorial Schedule:

Duration: 1 day

Part I:	Introduction into formal methods and Event-B	presentation, demo
Part II:	Model development by refinement	presentation, demo, joint work with the tool
Part III:	Modeling and verification of system dependability properties (safety analysis, safety cases and modeling fault tolerance)	presentation, demo, joint work with the tool
Part IV:	The Event-B ecosystem	presentation

Biographies:

Alexei Iliasov is a Research Associate at the School of Computing Science, Newcastle University, Newcastle-upon-Tyne, UK. He got his PhD in Computer Science in 2008 in the area of modeling artifacts reuse in formal developments. His research interests include agent systems, formal methods for software engineering, and tools and environments supporting modeling and proof. He has been involved in RODIN and DEPLOY and worked closely with Bosch, SAP and Space Systems Finland.

Linas Laibinis is an Adjunct Professor at the Department of Information Technologies of Abo Akademi University, Finland. He got his PhD in Computer Science in 2000 on mechanized formal reasoning about computer programs. His research interests include interactive environments for proof and program construction, as well as application of formal methods to modeling and development of fault tolerant and distributed software systems. He has been involved in RODIN and DEPLOY and worked closely with NOKIA and Space Systems Finland.

Elena Troubitsyna is an Associate 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 program committees of international conferences. Recently Elena has coordinated a Dagstuhl seminar on methods, models and tools for engineering resilient systems. She has been involved in preparation and running of RODIN and DEPLOY EU projects and worked closely with Bosch, SAP and Space Systems Finland.

Alexander Romanovsky is a Professor at the School of Computing Science, Newcastle University (UK), where he leads the Dependability Research Group. In 2008-2012 he was the coordinator of the FP7 DEPLOY Integrated Project on Industrial Deployment of System Engineering Methods Providing High Dependability and Productivity. Before this he coordinated the FP6 RODIN STREP on Rigorous Open Development Environment for Complex Systems. His main areas of research interests are dependability, fault tolerance mechanisms, fault tolerance reuse, exception handling and fault tolerance software architectures.