Modularisation in Event-B

Alexei Iliasov

(Newcastle)

The talk will present a novel composition/decomposition approach developed for the Event-B method. It is based on introducing the concepts of modules and module interfaces, and relies on machine decomposition using the intuitive operation call metaphor. The talk will describe the motivations for introducing the approach and demonstrate its soundness. We will introduce the modularisation plugin supporting modularisation within the Rodin Toolkit and show a brief demo. Some common patterns of model structuring will be discussed and illustrated with a case study. We will report on a substantial development of an industrial midium-scale application from the aerospace domain, in which the modularisation approach has been extensively used. This work is a result of collaboration between Newcastle University, Abo Akademy and Space Systems Finland within the ICT DEPLOY Integrated Project. More information can be found at http://wiki.event-b.org/index.php/Modularisation_Plug-in.
Tuesday 30th November 2010, 14:00
Robert Recorde Room
Department of Computer Science