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, châines 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'\'echantillonnage préefé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.