Les résultats attendus du projets sont de trois types :
des avancées scientifiques validées par des publications ;
des systèmes de vérification, simulation ou test,
sous forme de logiciels libres ;
des expérimentations sur des applications.
Les publications porteront sur des logiques, langages
de spécification, algorithmes de vérification
ou de génération de séquences de tests
prenant en compte des propriétés de nature quatitative
(complexité, temps-réel, stochastique)
et plus généralement sur les améliorations effectuées sur les calculs
existants (modularité, raisonnement équationnel model checking
compositionnel).
Les systèmes logiciels implémentant ou consolidant ces avancées
seront en source ouvert,
dans la continuité de ceux qui sont disponibles actuellement
(Coq, Elan, CMC, interfaces produites par CRIL).
Les résultats d'expérience portant sur des protocoles
publics comme PGM ou PIM seront également rendus publics.
Les OS temps-réel embarqués susceptibles d'être étudiés
ne sont pas, aujourd'hui, dans le domaine du logiciel libre.
Les études portant sur de telles applications
devront donc être soumises à des accords de confidentialité
appropriés.
Notons que derrière ces études se profile le marché
représenté par les terminaux portables, qui est considérable.
Toutefois le présent projet est de nature
exploratoire : son ambition est de préparer des technologies
de vérification applicable à ce contexte,
mais pas, dans l'immédiat, d'apporter
des solutions toutes prêtes.
Par ailleurs, toute la communauté des utilisateurs
de techniques de vérification formelle
bénéficiera des retombées de ce projet.
Parmi les sociétés mentionnées ci-dessus qui
ont des compétences fortes sur les systèmes et techniques
traités dans ce projet sans en être partenaires,
on peut mentionner
par exemple Trusted Logic et Dassault Aviation.
