[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS] Tutorial: Correct-by-Construction Development of Dependable Systems at ICFEM 2012



Tutorial announcement
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 
be discussed. 

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/