Guest speaker from France
Formal Models and Event B
The validation of formal specifications is a challenging task. It is one of the factors that impede the penetration of formal methods into the common practices of software development. In his talk he discussed the issue of validating formal models by executing them in the context of Event-B. The most important problem lies in the nondeterminism which often prevents purely automatic tools to execute models. In this talk, he first presented and discussed the techniques he has created to allow the execution of models at all levels of abstraction. These techniques rely on users to overcome the barriers resulting from nondeterministic features by either modifying the model or providing ad hoc implementations. Then, he presented JeB - the tool to execute models at any development stage. As validation is a relatively new concern in the formal methods community, he presented a few practical and theoretical problems that need to be tackled in the upcoming years.
Dr. Jean-Pierre Jacquot is an associate professor at Université de Lorraine, France since 1988. His interests lie in innovative teaching techniques, curriculum administration, and software engineering. His current research interest is with formal methods, Event-B particularly, and more specifically with the use and diffusion of such techniques among practitioners. At present, he focuses on the problem of validating formal models during their elaboration. He aims to provide tools and methodologies to integrate seamlessly validation into formal environments.