论文标题
证明定时BüchiAutomata的空虚
Certifying Emptiness of Timed Büchi Automata
论文作者
论文摘要
定时自动机的模型检查器被广泛用于验证安全至关重要的实时系统。最先进的工具通过复杂的抽象实现可扩展性。我们旨在进一步提高其验证结果的信任，尤其是用于检查Livices属性。为此，我们开发了一种方法，用于从模型检查运行中提取定时Büchi自动机的空虚证书。这些证书可以通过我们在Isabelle/Hol中正式验证的认证者进行仔细检查。我们在抽象环境中研究Livices证书，并表明我们的方法是合理而完整的。为了证明其可行性，我们提取了由Tchecker和Mimitator检查的几种模型的证书，并使用我们的经过验证的认证符对其进行验证。
Model checkers for timed automata are widely used to verify safety-critical, real-time systems. State-of-the-art tools achieve scalability by intricate abstractions. We aim at further increasing the trust in their verification results, in particular for checking liveness properties. To this end, we develop an approach for extracting certificates for the emptiness of timed Büchi automata from model checking runs. These certificates can be double-checked by a certifier that we formally verify in Isabelle/HOL. We study liveness certificates in an abstract setting and show that our approach is sound and complete. To also demonstrate its feasibility, we extract certificates for several models checked by TChecker and Imitator, and validate them with our verified certifier.
