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
- Activity report 2014-2019
- Activity report 2009-2014
- Activity report 2005-2009
- Activity report 2002-2005