Team

VESONTIO   (VESONTIO)

Description

The programme adresses the validation of systems by Model-Based Testing (MBT). It aims to evaluate the conformity between an implementation and a model of a system. The programme covers many research domains such that the modelization of the requirements, the test generation strategies and its technologies, the definition of test coverage criteria. The maturity of the results have allowed to create the start-up "Smartesting" seven yeras ago. A common research dynamic is started since 2004.

Our works are based on models. They necessitate the control of quality and an operational semantics of the different modelization languages (UML/OCL, B, JML...). We acquired a good experience in various paradigms of object modelling , pre/post and also for the annotation of code. These models allow to capture the functional aspect of the systems. They can be enriched by means of properties to describe the other aspects as in particular the security (integrity, confidentiality and availability of the systems). At present, we turn to the micro-systems and in a more general way to the complex embedded systems. These domains require to study new languages of modelling adapted to this sort of systems, such as SysML.

On the basis of these elements of modelling, we define coverage criteria for the generation of tests. They can be static because based on the analysis of the elements of modelling. They can also be dynamic because computed during the interpretation of these elements. The dynamic aspect raises problems because the systems to be taken into account are often very large-sized or infinite. To resolve this problem, we study methods of abstraction calculating under-approximations adapted to the generation of tests and\or to the classes of applications.

To make the interpretation of the elements of modelling, we are interested in various approaches as the  constraint solvers (CSP) and the solvers modulo theory ( SMT). Indeed, the works previously led by the team on the symbolic animation of specifications, showed the possibility of using a set solver of constraints for an efficient representation of objects. We plan to deepen this track subject in the objective to validate an object code  with regard to its specification, that it is about invariants, about postconditions of methods, or about more specific properties of security which express themselves by annotations at the level of the code.