• Automata Theory
• Concurrency
• Model Checking
• Probabilistic Systems
• Real-time Systems
• Security

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.


In multilevel systems it is important to avoid unwanted indirect
information flow from higher levels to lower levels, namely the so called
covert channels. Initial studies of information flow analysis were
performed by abstracting away from time and probability. It is already
known that systems which are considered to be secure may turn out to be
insecure when time or probability are considered. Recently, work has been
done in order to consider also aspects either of time or of probability,
but not both. In this thesis, a general framework is proposed, which is
based on Probabilistic Timed Automata, where both probabilistic and timing
covert channels can be studied. A concept of weak bisimulation for
Probabilistic Timed Automata is given, together with an algorithm to
decide it. Such an equivalence relation is necessary to define information
flow security properties. Thus, a Non Interference security property and a
Non Deducibility on Composition security property are given. They allow
expressing information flow in a timed and probabilistic setting, and they
can be compared with analogous properties defined in settings where either
time or probability or none of them are taken into account. This permits a
classification of the properties depending on their discriminating power.


Some new aspects are then explored involving the introduction of
parameters in Markov Decision Processes and the use of Timed Automata in
the study of cryptographic protocols. Finally, some real-life applications
are described through automata-based formalisms, and model checking is
used to study security issues affected by aspects of time and probability.