You are here
Verification and validation of software and embedded systems
VESONTIO has been the team’s name since 2008; before it was TFC (formal techniques with constraints).
The VESONTIO team is specialised in software quality and develops work to improve or analyse the reliability, security or performance of systems. The approaches are based on formal modelling of of both the systems under study and the specifications. At first line of work focuses on formal and semi-formal modelling, in particular on SysML and composite systems. A second strong axis studies how to test systems efficiently and automatically. Finally, a third axis around verification or automatic proof is being developed, recently with first results on quantum programs.
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. 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.