@unpublished{deploy144,
           title = {On Event-B and Control Flow 
},
          author = {Alexei Iliasov},
       publisher = {DEPLOY Project},
            year = {2009},
             url = {http://deploy-eprints.ecs.soton.ac.uk/144/},
        abstract = {Event-B is a general purpose formal development method 
suitable for the design and detailed development of safety-critical systems. Being a data-driven formalism, it lacks any control ?ow constructs. This turns out to be a limitation for systems with rich control ?ow properties. In Event-B, control ?ow information has to be embedded into 
guards and event actions and this results in an entanglement of control ?ow and functional specification with the additional downside of extra model variables. This paper proposes a method for extending Event-B  models with an new viewpoint portraying control ?ow properties of a 
model. The novelty of the work is in relying solely on theorem proving to demonstrate the consistency of control ?ow and main Event-B specification. The focus is placed on the practicality of working with such  an extension and also on achieving proof economy. A detailed formal 
treatment of the method is presented and illustrated with a case study.  A proof of concept implementation for the RODIN platform is brie?y discussed. 
}
}

<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>