Probabilistic timed automata (PTAs) are a formalism for modelling systems whose behaviour incorporates both probabilistic and real-time characteristics. Applications include wireless communication protocols, automotive network protocols and randomised security protocols. This paper gives an introduction to PTAs and describes techniques for analysing a wide range of quantitative properties, such as "the maximum probability of the airbag failing to deploy within 0.02 seconds", "the maximum expected time for the protocol to terminate" or "the minimum expected energy consumption required to complete all tasks". We present a temporal logic for specifying such properties and then give a survey of available model-checking techniques for formulae specified in this logic. We then describe two case studies in which PTAs are used for modelling and analysis: a probabilistic non-repudiation protocol and a task-graph scheduling problem.

Model Checking for Probabilistic Timed Automata

SPROSTON, Jeremy James
2013-01-01

Abstract

Probabilistic timed automata (PTAs) are a formalism for modelling systems whose behaviour incorporates both probabilistic and real-time characteristics. Applications include wireless communication protocols, automotive network protocols and randomised security protocols. This paper gives an introduction to PTAs and describes techniques for analysing a wide range of quantitative properties, such as "the maximum probability of the airbag failing to deploy within 0.02 seconds", "the maximum expected time for the protocol to terminate" or "the minimum expected energy consumption required to complete all tasks". We present a temporal logic for specifying such properties and then give a survey of available model-checking techniques for formulae specified in this logic. We then describe two case studies in which PTAs are used for modelling and analysis: a probabilistic non-repudiation protocol and a task-graph scheduling problem.
2013
43
2
164
190
G. NORMAN; D. PARKER; J. SPROSTON
File in questo prodotto:
File Dimensione Formato  
NPS-fmsd13_4aperto.pdf

Accesso aperto

Tipo di file: POSTPRINT (VERSIONE FINALE DELL’AUTORE)
Dimensione 624.2 kB
Formato Adobe PDF
624.2 kB Adobe PDF Visualizza/Apri
art%3A10.1007%2Fs10703-012-0177-x.pdf

Accesso riservato

Tipo di file: PDF EDITORIALE
Dimensione 1.06 MB
Formato Adobe PDF
1.06 MB Adobe PDF   Visualizza/Apri   Richiedi una copia

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/2318/143907
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 100
  • ???jsp.display-item.citation.isi??? 72
social impact