Keynote

Speaker: Prof. Marc Pantel - Associate Professor in Computer Science, University of Toulouse, Institut de Recherche en Informatique de Toulouse (IRIT).

Title: Property driven approaches to formal verification for domain specific modeling languages

Abstract

Most of the time, generic automated formal verification techniques do not scale well to realistic system design models and require costly verification specific model development. Indeed, for each property that must be assessed, the developer will abstract the verification model from the design model iteratively until verification can be conducted in a suitable time. Then, each change to the design model will require appropriate changes to the various verification models. Property driven verification approaches advocate the use of languages or tools dedicated to specific kind of properties in order to translate automatically design models to verification models whose automated verification scales better that the one of generic approaches. For example, instead of providing a very expressive logic like LTL (Linear Temporal Logic) that allows expressing relations between all events that can occur during the life of an executable model and require a generic translation from the design to verification models preserving all kind of events, the designer will only express more abstract requirements that can be translated more efficiently by abstracting all the events that are not meaningful for the requirements. The use case of real time properties for UML models will be used to illustrate this approach. One key point is that this approach requires building domain and property specific verification tools. The development process for such tools will also be illustrated including simple meta-tools that ease this development.

About the speaker

Marc Pantel (http://pantel.perso.enseeiht.fr) is associate professor at the University of Toulouse, France, in the Computer Science department of ENSEEIHT (http://www.enseeiht.fr). He conducts his research activities at IRIT (http://www.irit.fr), the Computer Science Research Institute in Toulouse, in the ACADIE team on Software Engineering for Safety Critical Systems. His work is focused on the practical use of Formal Methods, and specially on Model Driven Engineering to ease both the use of Formal Methods and the development of MDE and FM tools. He has been involved in many cooperative projects with major industrial partners like Airbus, Continental, SAFRAN and THALES.