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.

Probabilistic Timed Automata for Security Analysis and Design

TROINA, ANGELO
2017

Abstract

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.
146
978-1548887544
Troina, Angelo
File in questo prodotto:
Eventuali allegati, non sono esposti

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11585/606129
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact