论文标题
定时自动机作为表达安全的形式主义：关于理论和实践的调查
Timed automata as a formalism for expressing security: A survey on theory and practice
论文作者
论文摘要
定时自动机是验证受时间限制的并发系统的常见形式主义。他们使用时钟扩展有限状态自动机，从而限制了位置中的系统行为并进行过渡。虽然定时自动机最初是为了安全而设计的（从广泛的正确性W.R.T.正式属性中），但它们被逐渐用于许多作品以保证安全属性。在这项工作中，我们回顾了过去二十年来研究定时自动机的安全属性的工作。我们特别回顾了理论作品，特别关注不透明度以及更实用的作品，特别关注攻击树及其扩展。我们得出有关开放观点以及工具支持的主要结论。
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.
