Correct-by-Construction Development of Dependable Systems
November 12th, 2012, Kyoto, Japan
at ICFEM 2012
Dependability-explicit development process helps to construct systems that
are robust, well structured and have a higher degree of dependability.
The tutorial will provide researchers and industry practitioners with a systematic
introduction into the formal dependability-explicit development process in Event-B.
The tutorial will explain the semantic basis of formal modelling and development
by refinement and demonstrate the use of an automated tool support – the Rodin
platform that provides an integrated environment for system modelling and
verification. We will start with small introductory examples that show the role of
formal modelling in the requirements engineering and highlight the importance
of modelling and proofs. We will then explain the principles of expressing safety
invariants, verification of safety by proofs as well as interplaying fault tolerance
and safety. The connection between the safety analysis (FMEA, fault trees,
probabilistic assessment), safety cases and formal development in Event-B will
The Event-B framework has been successfully used in various industrial settings
and has a mature automatic tool support – the Rodin platform. Our work in
a succession of major EU projects (RODIN - http://rodin.cs.ncl.ac.uk/, DEPLOY -
http://www.deploy-project.eu/) has allowed us to gain considerable experience
in Event-B modelling of dependable systems in various industrial domains
(automotive, aerospace, transportation, business information, microprocessor
design). The tutorial will overview our experience in these areas.
The tutorial will be run in a highly interactive manner. With the help of the tutors
the participants will conduct a requirements analysis, create and refine formal
models as well as run proofs to verify model correctness. They are encouraged
to bring their own laptops to obtain the first-hand experience in modelling,
refinement and proofs in the Rodin platform.
Tutors: Alexei Iliasov, Linas Laibinis, Elena Troubitsyna, Alexander Romanovsky
(Newcastle University, Aabo Akademi University)
Tutorial web site: http://www.rodintools.org/tutorial.html
ICFEM 2012 web site: http://www.jaist.ac.jp/icfem2012/