作为安全表达形式化工具的时序自动机：理论与实践的综述
密码学与安全
2022-06-08 v1 形式语言与自动机理论
计算机科学中的逻辑
摘要
时序自动机是用于验证受时序约束并发系统的常见形式化工具。它们以时钟扩展有限状态自动机，时钟约束系统在各位置的行为并用于触发转移。尽管时序自动机最初为安全性（广义上相对于形式化属性的正确性）而设计，但渐进地，众多工作将其用于保障安全性质。本文综述近二十年来研究时序自动机安全性质的工作。我们重点综述理论工作，尤其关注不透明性，以及更偏实践的工作，尤其关注攻击树及其扩展。我们得出了关于开放前景与工具支持的主要结论。
引用
@article{arxiv.2206.03445,
title = {Timed automata as a formalism for expressing security: A survey on theory and practice},
author = {Johan Arcile and Étienne André},
journal= {arXiv preprint arXiv:2206.03445},
year = {2022}
}
备注
This is the author version of the manuscript of the same name published in ACM Computing Surveys