"Model Checking" Stichastique pour la performabilité et la sûreté des systèmes – CHECK-BOUND

L'utilisation généralisée des syst`emes automatis´es dans tous les aspects de nos vies donne une importance
incontestable `a la sˆuret´e de leur fonctionnement. La pr´esence de tels syst`emes dans des applications
critiques, coupl´ee `a leur complexit´e croissante, rend indispensable leur v´erification pour s'assurer qu'ils
se comportent comme pr´evu. Ainsi le ”model checking” qui est la mise en application des techniques
formelles de v´erification a un int´eret fondamental dans ce contexte. L'extension naturelle des techniques
de v´erification, qui sont devenues efficaces et r´epandues, ´etait l'´elargissement de mod`eles et de formalismes
de sp´ecifications auxquels le ”model checking” peut ˆetre appliqu´e. De plus, puisque les comportements
des syst`emes r´eels sont stochastiques, le formalisme a ´et´e ´etendu au ”model checking” probabiliste.
Differents formalismes dans lesquels le syst`eme consid´er´e est d´efini par une chaˆine de Markov ont ´et´e
propos´es et la v´erification des mod`eles markoviens peut ˆetre effectu´ee par analyse num´erique ou par
simulation. Dans le formalisme ”model checking”, les mod`eles consid´er´es sont v´erifi´es pour d´ecider si
des contraintes sur les mesures ´etudi´ees sont satisfaites sans n´ecessairement connaˆitre la valeur exacte
de chaque mesure. De ce fait, il est possible d'appliquer les m´ethodes de bornes : on peut valider un
mod`ele `a partir des mesures bornantes. Si la borne v´erifie la contrainte impos´ee alors le mod`ele est
v´erifi´e, sinon on ne peut pas d´ecider et il faut raffiner le mod`ele bornant pour am´eliorer la qualit´e de
la borne. Nous proposons donc d'appliquer les m´ethodes de Comparaison Stochastique qui permettent
de construire des bornes sur les distributions transitoires et la distribution stationnaire. Nous proposons
´egalement d'appliquer l'approche par simulation parfaite avec le couplage dans le pass´e dont l'efficacit´e a
´et´e d´emontr´ee pour calculer la distribution stationnaire lorsque le mod`ele est monotone. Nous envisagons
d'´elargir cette approche pour l'analyse transitoire et pour le ”model checking” des mod`eles bornants `a
l'aide de la monotonie stochastique. L'approche par bornes peut ´egalement apporter une solution dans le
cadre du ”model checking” infini qui est un probl`eme difficile `a aborder.
De nombreux liens existent entre la v´erification formelle utilisant le ”model checking” et l'´evaluation
quantitative de performance et de disponibilit´e. Notre grande exp´erience dans le cadre de l'´evaluation
quantitative permettra sans aucun doutes d'obtenir des r´esultats int´eressants dans le contexte du ”model
checking” stochastique.