Equipe de recherche CASSIS
Cassis is a joint project between the LORIA (Laboratoire Lorrain de Recherche en Informatique et ses Applications, UMR 7503) and FEMTO-ST (Franche-Comté Electronique Mécanique Thermique et Optique - Sciences et Technologies, UMR 6174).
The objective of the project is to design and develop tools to verify the safety of systems with an infinite number of states. The analysis of such systems is based on a symbolic representation of sets of states in terms of formal languages or logical formulas. Safety is obtained via automatic proof, symbolic exploration of models or test generation. These validation methods are complementary. They rely on the study of accessibility problems and their reduction to constraint solving.
An originality of the project is its focus on infinite systems, parameterized or large scale, for which each technique taken separately shows its limits. This is the case for example with protocols operating on topologies of arbitrary size (ring networks), systems handling data structures of any size (sets), or whose control is infinite (automata communicating through an unbounded buffer). Ongoing or envisioned applications concern embedded software (e.g., smart cards, automotive controllers), cryptographic protocols (IKE, SET, TLS, Kerberos) designed to ensure trust in electronic transactions, and distributed systems.
The problem of validating or verifying reactive systems is crucial because of the increasing number of security-sensitive systems. The failure of these critical systems can have dramatic consequences since they may be embedded in vehicle components, or they control power stations or telecommunication networks. Besides obvious security issues, the reliability of products whose destination is millions of end-users has a tremendous economical impact.
There are several approaches to system verification: automated deduction, reachability analysis or model-checking, and testing. These approaches have different advantages and drawbacks. Automated deduction can address practical verification, however it remains complex to handle and requires a lot of expertise and guidance from the user. Model-checking is exhaustive but must face combinatorial explosion and becomes problematic with large-size or infinite systems. Testing is fundamental for validating requirements since it allows the discovery of many errors. However, it is almost never exhaustive and therefore only leads to partial solutions. Hence we believe that these approaches should not be considered as competing but as complementary.
The goal of our project is to contribute to new combinations of these three verification techniques in a framework that would apply them in an industrial context. In particular we expect some breakthrough in the infinite-state verification domain by joint applications of deductive, model-checking and testing techniques.
est arrêtée depuis le 31/12/2015
En savoir plus
Retrouvez sur le site web RAweb
- le rapport d'activité complet de l'équipe CASSIS (en anglais)
- le rapport d'activité de toutes nos équipes de recherche (en anglais)
- Rapport d'activité complet 2015
- Rapport d'activité complet 2014
- Rapport d'activité complet 2013
- Rapport d'activité complet 2012
- Rapport d'activité complet 2011
- Rapport d'activité complet 2010
- Rapport d'activité complet 2009
- Rapport d'activité complet 2008
- Rapport d'activité complet 2007
- Rapport d'activité complet 2006
- Rapport d'activité complet 2005
- Rapport d'activité complet 2004
- Rapport d'activité complet 2003