The VELO team studies formal methods for the modelling and analysis of models for complex systems. These systems can be of any type, but we are particularly interested in the modelling of large-scale natural systems (from the environment) and software systems. Our main objects of study are models, whatever their origin. We study and develop modelling formalisms adapted to the contexts in which our systems evolve (semi-formal, formal, discrete-event, continuous, probabilistic, hybrid, etc.), as well as the associated verification techniques (software testing, formal proof, model-checking, statistical analysis).

Complex systems that interact with various physical or software components, large data sets, time constraints, robustness and quality requirements are difficult to model and develop.
 
We tackle these difficulties through different themes that revolve around models, from their construction to their analysis. The study of models is then declined according to different facets which constitute a complex system:

• The agents/services and components that interact in the system;
• Analysis of heterogeneous systems;
• System architecture and evolution;
• Various semantic models (e. g. logical, state, component, service, discrete event, probabilistic, timed, etc.) and associated verification techniques.

• Correct software components
• Multiformalism and multifaceted system analysis
• Software architecture
• Probabilistic models, competition semantics, associated verification tools

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.