En évaluation quantitative de la sécurité et de la performabilité, les
verrous sont de deux ordres : comment spécifier et obtenir les états
et les transitions d'un système complexe dans un formalisme
se prêtant aux calculs et ensuite comment effectivement réaliser ces
calculs. Le premier problème a été en partie réglé par les
représentations tensorielles initiées par nos équipes via le formalisme
des RAS (Réseaux d'Automates Stochastiques)
et qui ont depuis été généralisées à toutes
les approches quantitatives modulaires (superposition de réseaux de
Petri, Algèbre de Processus, chaînes de Markov en
interaction) par diverses équipes
Françaises, Européennes ou Américaines (Haddad en France, Donatelli,
Buchholz, et Kemper en Europe, Ciardo et Stewart aux USA).
Par contre, les algorithmes de
calcul ne pourront jamais résoudre les problèmes de ces
tailles. C'est pourquoi nous proposons diverses méthodes de biais (en
simulation)
ou
de bornes (pour les calculs numériques)
permettant de travailler sur des modèles stochastiques plus
simples (plus petits, ou plus réguliers, ou avec une plus grande
fréquence pour une transition remarquable). Ces algorithmes permettent
de donner des garanties plutôt que des valeurs exactes et permettent
donc un ``model checking'' stochastique et la vérification de
contraintes quantitatives de sureté.
Les approches tensorielles ont
déjà été appliquées dans le contexte du ``model checking''
stochastique
(APPN par Buchholtz) et les approches de bornes sur les probabilités
sont de plus en plus fréquentes dans le contexte des systèmes à grand
espace d'états (travaux de Buchholtz sur l'approche de Courtois et les
produits tensoriels à Performance 2002,
travaux de Donatelli, Moreaux et Haddad sur une approche mixte
Courtois et trajectoires, tutoriel de Fourneau à Performance 2002 sur
les approches algorithmiques des bornes trajectorielles).
En simulation l'échantillonnage préférentiel
(importance sampling)
et la
ramification de trajectoires (importance splitting)
ont été étudiés par
les équipes ayant les contributions méthodologiques
les plus importantes du domaine
(voir les travaux de Nakayama, Nicola, Heidelberger, Shahabuddin,
Glasserman et Villen). Les équipes sont complémentaires aussi bien
pour les approches numériques (analyse
Markovienne de la sureté dans ARMOR, approche tensorielle et bornes
numériques
dans ID et PRiSM) et de simulation (Monte Carlo dans ARMOR, couplage
dans le passé et parallélisme dans PRiSM et ID).
Cette collaboration s'appuie aussi sur des colloborations
internationales dans les laboratoires avec des spécialistes reconnus
du domaine: ID avec Stewart, Ciardo et Donatelli (via CNRS-NSF),
et PRiSM avec Stewart (via CNRS-NSF), Hillston,
et Dayar pour la modélisation Markovienne,
ARMOR avec H. Cancela et K. Trivedi pour la simulation.