Timed automata as a formalism for expressing security: A survey on theory and practice

Abstract

Timed automata are a common formalism for the verification of concurrent systems subject to timing constraints. They extend finite-state automata with clocks, that constrain the system behavior in locations, and to take transitions. While timed automata were originally designed for safety (in the wide sense of correctness w.r.t. a formal property), they were progressively used in a number of works to guarantee security properties. In this work, we review works studying security properties for timed automata in the last two decades. We notably review theoretical works, with a particular focus on opacity, as well as more practical works, with a particular focus on attack trees and their extensions. We derive main conclusions concerning open perspectives, as well as tool support.

This is the author version of the manuscript of the same name published in ACM Computing Surveys

References in corpus (5)

• What's decidable about parametric timed automata?
• Attack Trees for Security and Privacy in Social Virtual Reality Learning Environments
• A Benchmarks Library for Extended Parametric Timed Automata
• Guaranteeing Timed Opacity using Parametric Timed Model Checking
• Corrections to A Menagerie of Timed Automata

Cited by in corpus (3)

• Configuring Timing Parameters to Ensure Execution-Time Opacity in Timed Automata
• Expiring opacity problems in parametric timed automata
• Execution-time opacity control for timed automata