Probabilistic Timed Automata for Security Analysis and Design

The usefulness of formal methods for the description and verification of complex systems is nowadays widely accepted. While some system properties can be studied in a non-timed and non-probabilistic setting, others, such as quantitative security properties, system performance and reliability properties, require a timed and probabilistic description of the system. This thesis focuses on methods for the formal modeling of probabilistic timed systems, and on algorithms for the automated verification of their properties. The models considered describe the behavior of a system in terms of time and probability, and the formal description languages used are based on extensions of Timed Automata, Markov Decision Processes and combinations of them. Bisimulation relations and model checking are used to define and verify security properties of probabilistic timed systems.