Towards Building Verifiable CPS using Lingua Franca
Towards Building Verifiable CPS using Lingua Franca
复制标题
DOI：
10.1145/3609134
复制
发表时间：
2023-09
影响因子：
2
通讯作者：
Shaokai Lin;Yatin A. Manerkar;Marten Lohstroh;Elizabeth Polgreen;Sheng-Jung Yu;Chadlia Jerad;Edward A. Lee;S. Seshia
中科院分区：
文献类型：
--
作者：
Shaokai Lin;Yatin A. Manerkar;Marten Lohstroh;Elizabeth Polgreen;Sheng-Jung Yu;Chadlia Jerad;Edward A. Lee;S. Seshia
网络物理系统（CPS）的形式化验证具有挑战性，因为它必须考虑实时性和并发性方面，而这些在普通软件中往往不存在。此外，CPS中的软件通常复杂且底层，这使得很难确保用于验证的系统形式化模型能忠实反映实际实现，这可能会削弱验证结果的价值。为了解决这个问题，我们提出了一种构建可验证CPS的方法，其基于软件的形式化模型可从其实现中自动推导出来的原则。我们的方法要求系统实现用Lingua Franca（LF）来指定，LF是一种为实时、并发CPS量身定制的多语言协调语言，我们通过代码中的注释使其适用于安全属性的规范。LF的程序结构和确定性语义使得能够直接从LF程序自动构建形式化公理模型。生成的模型由验证引擎Uclid5使用Z3 SMT求解器通过有界模型检查（BMC）进行自动检查。所提出的技术能够检查安全度量时态逻辑（Safety MTL）公式的一个明确定义的片段。为了确保BMC的完整性，我们提出了一种基于LF语义推导公理模型完整性阈值上限的方法。我们在LF验证器中实现了我们的方法，并使用一个基准测试套件对其进行评估，该套件包含从现实应用以及针对Erlang、Lustre、面向角色的语言和实时操作系统的基准测试中抽取的22个程序。LF验证器能够自动正确检查22个程序中的21个。
Formal verification of cyber-physical systems (CPS) is challenging because it has to consider real-time and concurrency aspects that are often absent in ordinary software. Moreover, the software in CPS is often complex and low-level, making it hard to assure that a formal model of the system used for verification is a faithful representation of the actual implementation, which can undermine the value of a verification result. To address this problem, we propose a methodology for building verifiable CPS based on the principle that a formal model of the software can be derived automatically from its implementation. Our approach requires that the system implementation is specified in Lingua Franca (LF), a polyglot coordination language tailored for real-time, concurrent CPS, which we made amenable to the specification of safety properties via annotations in the code. The program structure and the deterministic semantics of LF enable automatic construction of formal axiomatic models directly from LF programs. The generated models are automatically checked using Bounded Model Checking (BMC) by the verification engine Uclid5 using the Z3 SMT solver. The proposed technique enables checking a well-defined fragment of Safety Metric Temporal Logic (Safety MTL) formulas. To ensure the completeness of BMC, we present a method to derive an upper bound on the completeness threshold of an axiomatic model based on the semantics of LF. We implement our approach in the LF Verifier and evaluate it using a benchmark suite with 22 programs sampled from real-life applications and benchmarks for Erlang, Lustre, actor-oriented languages, and RTOSes. The LF Verifier correctly checks 21 out of 22 programs automatically.