VELO - Checking for Environment and Software
Correct software components
The challenge of building by composition of basic elements is faced here. The objective is to propose simple concepts and techniques for assembling components and services while guaranteeing the correction, through formal models and methods, of verification techniques (proofreading, state exploration, testing). In particular, we explore techniques for testing model transformations.
Multiformalism and multifaceted system analysis
Heterogeneity in composition is one of the characteristics of complex systems; here we address the challenge of interoperability and global software analysis, modular model development and compositional model analysis.
The challenge of building by composition of basic elements is faced here with a top-down approach. The objective is to describe and study the global architecture of the software and closely study the study of the compound services that interact in the software. As the software evolves over time (according to the requirements of its environment), taking into account the evolution at different stages is one of our fields of study.
Probabilistic models, competition semantics, associated verification tools
Controlling the complexity of software requires the development of appropriate formal models and their analysis to ensure that the expected properties and the absence of unwanted properties are ensured. We study here, models based on automata and in particular continuous-time and probabilistic models.
In relation to these themes, the skills of the team members allow us to explore in particular :
- models for services, components and global architecture;
- methods of verification by evidence, state exploration and testing;
- reactive, competitive, embedded and information systems;
- natural systems with continuous or hybrid behavior.