Generalized Property-Directed Reachability for Hybrid Systems
Generalized Property-Directed Reachability for Hybrid Systems
复制标题
DOI：
10.1007/978-3-030-39322-9_14
复制
发表时间：
2019-10
期刊：
影响因子：
--
通讯作者：
Kohei Suenaga;T. Ishizawa
中科院分区：
文献类型：
--
作者：
Kohei Suenaga;T. Ishizawa
广义属性导向可达性（GPDR）属于IC 3/PDR模型检测技术家族。它已成功应用于软件验证;例如，它是Spacer的核心，Spacer是与Z3捆绑在一起的最先进的Horn子句求解器。然而，它还没有被应用到混合系统，其中涉及一个不断演变的价值观随着时间的推移。作为基于GPDR的混合系统模型检验的第一步，本文形式化了GPDR对混合系统的适应，并证明了其合理性。我们还实现了一个半自动的概念验证器，它允许用户提供提示来指导验证步骤。
Generalized property-directed reachability(GPDR) belongs to the family of the model-checking techniques called IC3/PDR. It has been successfully applied to software verification; for example, it is the core of Spacer, a state-of-the-art Horn-clause solver bundled with Z3. However, it has yet to be applied to hybrid systems, which involve a continuous evolution of values over time. As the first step towards GPDR-based model checking for hybrid systems, this paper formalizes, an adaptation of GPDR to hybrid systems, and proves its soundness. We also implemented a semi-automated proof-of-concept verifier, which allows a user to provide hints to guide verification steps.