The research of the VASCO team addresses modeling, verification and validation (V&V) of systems. Models play a key role in our V&V activities. On the one hand, they may provide a reference vs which some implementation can be verified. On the other hand, an existing system can be modelled and its model can then be verified giving some clues on the correctness of the actual system. In both cases, models must be validated, i.e. it should be shown that the model corresponds to the existing reality or to the needs of the customer.

The major industrial V&V activity is testing. The researches of the VASCO team are historically dedicated to testing. In the testing context, models play two roles: executable models can be used as oracles for the test, and model-based testing can generate test cases from a model.

The researches of the VASCO team pursue the following orientations:

Models as oracles

During the last five-years period, we dedicated significant efforts to the MODMED ANR project (2015-2019), which aimed at defining a language to express properties of execution traces. These properties play the role of a partial model, and can be evaluated on the traces. These traces can be produced by the execution of test cases, but also can be collected from the usage of the system.

Inferring models for test generation

In the recently started Philae ANR project (2018-2022), we still focus on traces collected from tests or from the usage of the system. But here, we exploit these traces to infer models of the system. These models will later be used to generate tests which themselves will produce new traces. They can also be studied to identify system faults.

Building models for verification

Building the model of a complex system is not an easy task. The VASCO team has a long experience of integrating graphical models (UML diagrams) and formal models (Z and B) for system verification. Since 2008, we are building the B4MSecure system which translates a Secure UML diagram, annotated with B assertions into B machines. The resulting formal model can then be verified using proof tools, model-checkers or animation.

Lightweight formal methods

Our research aims at facilitating the work of software engineers. This can be achieved by providing automation. Therefore most of our researches end up with the development of tools (e.g. SIMPA, ParTraP-IDE, B4MSecure/Meeduse). The lightweight approach to formal methods can also be achieved by supporting well-accepted modeling languages, such as UML, or designing intuitive languages such as ParTraP, our language to express trace properties.

In order to better understand the capabilities of our research, it is systematically applied to case studies. In the last 5 years, we have applied our research to the field of security, but also to the modelling of railway systems, and the verification of medical systems (computer-aided surgery).

Activity reports

Competence sheet of the VASCO team (2013)

Faits marquants

L'outil Meeduse gagne le prix "Best Verification" (2019)

L'outil Meeduse développé au sein de l'équipe VASCO et porté par Akram Idani, a gagné le prix "Best Verification" lors de la 12ème édition du Transformation Tool Contest ( La compétition s'est déroulée à Eindhoven (Pays-Bas) avec les conférences ECMFA et ICMT, et a réuni sept compétiteurs. Le but de cet événement est de comparer selon divers critères (i.e. expressivité, correction, performances...) des outils de transformation de graphes, de modèles et de programmes au moyen d’études de cas. Cette année l'étude de cas choisie porte sur la transformation de tables de vérité (Truth Tables) en diagrammes de décision binaires (Binary Decision Diagrams). La solution apportée par Meeduse permet l'usage d'outils de raisonnement formel (prouveurs et model-checkers) et s'est distinguée par sa correction et sa rigueur. Meeduse a également été classé troisième sur le "Audience award". Pour les détails techniques, rendez-vous sur la page de l'outil (

Amira Radhouani présente son travail de thèse