Confiance, Preuve et Probabilités – CPP

Dans le cadre de la validation des propriétés de sûreté des programmes critiques, le projet CPP étudiera l?utilisation conjointe des méthodes probabilistes et formelles, dans le but d?améliorer la précision et la classe d?application des méthodes d?analyse statique de programmes numériques. Les programmes en C sont souvent vu comme des programmes déterministes. Cependant, les programmes numériques que nous nous proposons d?étudier dans ce projet ont également des aspects probabilistes et non-déterministes. Les aspects probabilistes proviennent généralement d?erreurs de mesure introduites par les capteurs. Les sources du non-déterminisme sont elles plus nombreuses. Tout d?abord, les valeurs d?entrée des programmes sont généralement prises dans un ensemble connu de valeurs et l?ajout d?une loi de probabilités sur ces entrées ne serait pas réaliste. Enfin, l?analyse des structures conditionnelles dans un programme introduit du non-déterminisme : on peut voir une instruction ?if b then e1 else e2? comme un adversaire que contrôle la branche (e1 ou e2) qui sera prise pour obtenir la plus grande erreur possible. Les participants au projet vont tout d?abord construite un ensemble de cas de tests provenant de codes industriels fournis par Hispano-Suiza. Cet ensemble de cas d?études vise à montrer l?utilité de ce projet en étudiant les techniques classiques de l?état de l?art (comme les simulations à la Monte-Carlo par exemple), et nous comparerons ces résultats avec ceux obtenus par les nouvelles techniques développées dans le projet. Ces comparaisons permettront de valider nos méthodes. Dans un deuxième temps, les participants poseront les bases théoriques des techniques d?analyses développées dans le projet. En s?appuyant sur l?expertise de certains des participants sur la sémantique à base de prévisions, nous construirons une nouvelle sémantique mélangeant déterminisme et probabilités pour les programmes numériques. Ensuite, nous définirons des approximations calculables des sémantiques précédemment définies. Nous pensons en particulier à une généralisation des P-boxes. Nous voulons également combiner cette approche avec une approche décrivant les programmes critiques comme un système hybride, si de l?information déterministe est disponible (par exemple, une description des entrées par un système d?EDOs). Une application très importante de ces abstractions est la caractérisation de la précision des calculs numériques des programmes à analyser. Des tests seront effectués dans le cadre du projet FLUCTUAT. Enfin, nous voulons améliorer notre vision des calculs numériques en présence d?incertitudes sur les données et/ou les paramètres. Notre idée est que nous ne pouvons pas éliminer un code dont le flot de contrôle « réel » (c?est-à-dire utilisant des nombres réels) et « flottant » (c?est-à-dire utilisant des nombres à virgule flottante) diffèrent. Les deux flots de contrôles peuvent en effet avoir malgré tout des résultats très proches. La distance de bi-simulation est une des directions de recherche que nous envisageons pour améliorer notre compréhension de la qualité des codes numériques.