Abstract FR:

Les methodes formelles et la surete de fonctionnement sont deux domaines connexes qui s'interessent a l'analyse des comportements des systemes critiques. Ces domaines adoptent des points de vue differents mais complementaires sur les systemes. Les methodes formelles considerent le point de vue fonctionnel et adoptent, en general, une approche verification de programme. Dans ce domaine on cherche en general a mettre en evidence un scenario menant le programme a un bogue, ou a generer de maniere automatique des programmes surs (par rapport a leurs specifications). La surete de fonctionnement considere plutot les aspects dysfonctionnels des systemes. Dans ce domaine on cherche a determiner les scenarios preponderants qui menent le systeme a une defaillance ou a evaluer des mesures probabilistes sur ses comportements (fiabilite, disponibilite,). Les travaux presentes dans cette these ont ete realises dans le cadre d'un projet industriel, altarica, qui ambitionne le rapprochement des methodes formelles et de la surete de fonctionnement. Cette unification se concretise par le developpement d'un atelier d'analyse systeme, l'atelier altarica, qui federera, a terme, un ensemble de modeles et d'outils pour l'analyse des systemes. Cet atelier propose une representation unique pour la description des systemes ; celle-ci etant destinee a etre compilee vers des modeles/outils existants. Ce rapport presente le formalisme supporte par cet atelier, sa forme textuelle et graphique (le langage altarica), certaines proprietes de sa semantique et quelques exemples de modelisations. L'etude des scenarios de panne est un des principaux problemes de la surete de fonctionnement. Ce probleme est generalement traite en utilisant le modele des arbres de defaillances. Ce modele ne permettant pas de prendre en compte le sequencement des pannes, cette these propose une solution au probleme de l'obtention des scenarios de panne minimaux pour l'ordre des sous-mots.