Autómatas estocásticos para sistemas concurrentes y tolerantes a fallas

Abstract

En esta tesis introducimos una nueva clase de autómata llamada Input/Output Stochastic Automata (IOSA). Los IOSA son composicionales, y los IOSA cerrados (sin acciones de entrada) son completamente deterministas y por lo tanto aptos para simulación. Esto los hace atractivos para analizar sistemas probabilistas complejos, que son imprácticos de analizar por Model Checking. Una segunda versión de IOSA introduce al modelo acciones urgentes, con el fin de mejorar la composicionalidad del modelo. Esta extensión introduce no-determinismo también el los modelos cerrados. Logramos distinguir no-determinismo espurio producido por acciones confluentes. Sumado a esto, proveemos condiciones suficientes para asegurar que una red de IOSAs que interactúan es determinista sin la necesidad de analizar el modelo compuesto. Finalmente, usamos IOSA con acciones urgentes para definir una semántica formal para Repairable Fault Trees (RFT), una técnica muy efectiva para el análisis de modelos industriales. Probamos que la semántica es determinista, y analizamos un caso de estudio usando el simulador de eventos raros FIG.

In this thesis we introduce a new class of automata called Input/Output Stochastic Automata (IOSA). IOSAs are compositional, and closed IOSAs (no input actions) are fully deterministic and therefore suitable for simulation. This makes them attractive for analyzing complex probabilistic systems, which are impractical to analyze by Model Checking. A second version of IOSA introduces urgent actions to the model, in order to improve the compositionality of the model. This extension introduces non-determinism also in closed models. We managed to distinguish spurious non-determinism produced by confluent actions. Added to this, we provide sufficient conditions to ensure that a network of interacting IOSAs is deterministic without the need to analyze the composite model. Finally, we use IOSA with urgent actions to define a formal semantics for Repairable Fault Trees (RFTs), a very effective technique for industrial model analysis. We prove that the semantics are deterministic, and we analyze a case study using the rare event simulator FIG.