You are here
Verification and validation of software and embedded systems
VESONTIO has been the team’s name since 2008; the prior name was TFC (formal techniques with constraints). A part of the team has been integrated into the dual-site project INRIA CASSIS (Nancy and Besançon).
The team’s specific expertise is in the combination of methods (automatic proof, model-checking, testing) for model-based verification and validation, the scientific lock being the combinatorial explosion of the size of system models to be analyzed. This activity is conducted along three different lines: modeling of large finite systems and finite systems, model-based automatic verification and validation (including the generation of tests), and scalability.
Goals and Research Areas
Our VESONTIO team has focused its efforts specifically on modeling, verification and automatic validation of embedded systems (ex.: smart cards and automobiles), component-based systems and services, as well as on the study of safety and security of communication systems and information.
With the evolution of the field’s themes and topics, particularly towards microsystems, new scientific challenges have been identified :
- Management of complexity through construction
- Management of component-based heterogeneous systems
- Management of uncertainty through adaptation/reconfiguration
From these scientific challenges, two themes of research emerge:
› Safety and reliability of communications and information systems : development of formal methods to verify and test the safety of communications systems, such as protocols or information systems. These problems are addressed through verification techniques, both on symbolic models (languages, automata, logic, rewriting, etc.), but also model-based tests (model covers, scenarios, etc.).
› Verification and testing of software components and embedded systems : design, modeling of safe and reliable systems. The approaches used are verification techniques for compound systems (Petri nets, interface controllers, etc.) and for model-based tests (model cover, test limits, etc.).
One of the VESONTIO team’s strengths is that it can bring together, within a single team, skills from different domains of software reliability: model checking, with model-supported evidence and testing.
Such eclecticism enables combinations of original approaches in order to confront common challenges jointly and as partners. Technological transfer to the company Smartesting has given rise to much industrial cooperation in the team’s scientific subject areas.
Implementing our work
In interdepartmental exchanges at FEMTO-ST, different needs have appeared at different scales in the fields of modeling, testing and simulations of complex systems. The latter include software aspects, but also physical phenomena, for example, of the mechanic, energy or quantum type. The department has participated in collaborative projects in these directions with the institute’s other departments.