creators_name: Iliasov, Alexei creators_name: Laibinis, Linas creators_name: Troubitsyna, Elena creators_name: Romanovsky, Alexander creators_id: "Alexei Iliasov" creators_id: Linas.Laibinis@abo.fi creators_id: Elena.Troubitsyna@abo.fi creators_id: alexander.romanovsky@ncl.ac.uk type: teaching_resource datestamp: 2011-08-02 12:57:38 lastmod: 2011-08-02 12:57:38 metadata_visibility: show title: Correct-by-Construction Development of Fault Tolerant Systems (Tutorial at FM 2011) ispublished: pub subjects: Event-Bsemantics subjects: Refinement subjects: deploy_method subjects: deploy_method_resil subjects: deploy_training full_text_status: none abstract: Ensuring system fault tolerance is one of the major concerns in developing critical industrial applications. The tutorial shows how to rigorously develop systems that are not only functionally correct but also fault tolerant. The material of the tutorial is built on the results of two EC projects, RODIN and DEPLOY, that created and validated in the industrial settings the RODIN platform - an Eclipse-based development environment supporting formal modelling in Event-B. The focus of the tutorial is on demonstrating how fault tolerance can be systematically specified and verified as an intrinsic part of the overall system behavior. The general principles are demonstrated by several industrial case studies based on our work with telecommunication, space and business information sectors. As part of the tutorial we will introduce and demonstrate a number of RODIN tools that support model structuring using modes, modules, and fault tolerance views, and facilitate fault tolerance modelling. All materials of this tutorial are available on http://iliasov.org/fm2011/ date: 2011 official_url: http://iliasov.org/fm2011/ related_url_url: http://sites.lero.ie/fm2011/Tutorial3.html citation: Iliasov, Alexei and Laibinis, Linas and Troubitsyna, Elena and Romanovsky, Alexander (2011) Correct-by-Construction Development of Fault Tolerant Systems (Tutorial at FM 2011). [Teaching Resource]