Speaker: Yamine Ait-Ameur
Abstract: In this talk, we will discuss state-based formal methods, namely the Event-B method. We report on our findings about the definition of algebraic theories that are utilised within Event-B model refinement chains. In our method, Event-B models borrow types, operators, axioms, theorems, proof and rewrite rules from these theories. Relying on their well-definedness, these operators, axioms, theorems and proof and rewrite rules are useful to discharge the proof obligations generated for these models, and contribute to reducing development efforts, as theorems of the theories are proved once and for all. The approach is illustrated on the generation of new proof obligations in particular for verifying cyber-physical systems.
Bio: Yamine AIT AMEUR is Full Professor since 2000. Since Sept 2011, he is at Toulouse INP (National Polytechnique Institute) in Toulouse (France) and member of the Toulouse research institute in computing (IRIT-CNRS). Two main important aspects characterize his research activities. On the one hand the fundamental aspects through the development and use of state based formal modelling techniques based on refinement and proofs, in particular Event-B and explicit formalisation of the semantics of domain knowledge using formalised ontology models. On the other, hand, practical aspects, through the development of operational applications, allowing to validate the proposed approaches. Embedded systems in avionics, engineering, interactive systems, CO2 capture are some of the application domains targeted by this work.