ICFEM 2012, November 12, 9:00 - 17:30



Correct-by-Construction Development of Dependable Systems

Download tutorial slides

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 has been successfully used in industrial setting and has a mature automatic tool support – the Rodin platform. A succession of several EU projects (RODIN - http://rodin.cs.ncl.ac.uk/, DEPLOY - http://www.deploy-project.eu/) 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.

Tutorial instructors:

  • Alexei Iliasov is a Researcher 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 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. He has been involved in RODIN and DEPLOY and worked closely with Bosch, SAP and Space Systems Finland
  • 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. He has been involved in RODIN and DEPLOY and worked closely with Space Systems Finland
  • 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 was a PC chair of SERENE 2011 - International Workshop on Software Engineering for Resilient Systems. She has been involved in preparation and running of RODIN and DEPLOY 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. He is 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.