Systèmes distribués, ouverts et temporisés – DOTS

Le projet DOTS porte sur la sp´ecification formelle et la v´erification automatique des syst`emes informatiques.
Plus particuli`erement il s'int´eresse aux syst`emes complexes, comme les fameux syst`emes embarqu
´es, qui int`egrent des aspects temporis´es (des contraintes temps-r´eel), des aspects distribu´es (ces
syst`emes contiennent plusieurs composants qui communiquent entre eux) et des aspects interactifs avec
leur environnement (on parle alors de syst`emes ouverts). Si chacun de ces aspects pris s´epar´ement est
aujourd'hui bien connu, la v´erification de syst`emes combinant plusieurs de ces caract´eristiques reste un
probl`eme largement ouvert.
L'objectif du projet DOTS est de permettre des avanc´ees th´eoriques et algorithmiques (valid´ees par
des prototypes) pour la conception de syst`emes temporis´es, distribu´es et ouverts. Une caract´eristique
essentielle du projet est de rassembler des sp´ecialistes de chacun des trois aspects mentionn´es ci-dessus
pour confronter les techniques propres `a chaque domaine et aborder conjointement la v´erification des
syst`emes complexes.
Nous nous int´eresserons principalement au model checking, mais aussi au probl`eme du contrˆole (comment
superviser un syst`eme pour qu'il v´erifie une propri´et´e de correction donn´ee ?) et au probl`eme de la noninterf
´erence (comment s'assurer qu'un syst`eme ne communique pas certaines informations sensibles `a un
observateur ext´erieur ?).
Pour attaquer ces probl`emes, nous travaillerons autour de deux approches particuli`eres. D'une part, nous
utiliserons le cadre des jeux pour mod´eliser et analyser les interactions des syst`emes. Et d'autre part,
nous utiliserons les m´ethodes `a base d'ordres partiels pour appr´ehender les aspects distribu´es. Combiner
ces techniques en y int´egrant aussi des contraintes temps-r´eel est une perspective novatrice et constitue
une sp´ecificit´e importante de notre projet.