Automated Predicate Abstraction for Real-Time Models
Automated Predicate Abstraction for Real-Time Models
复制标题
DOI：
10.4204/eptcs.10.3
复制
发表时间：
2009-11
期刊：
影响因子：
--
通讯作者：
Bahareh Badban;S. Leue;J. Smaus
中科院分区：
文献类型：
--
作者：
Bahareh Badban;S. Leue;J. Smaus
模型检测在验证和调试硬件设计和通信协议方面取得了广泛的成功。然而，状态空间爆炸是一个固有的问题，限制了模型检测工具的适用性。为了克服这一限制，软件模型检查者提出了不同的方法，其中抽象方法受到高度重视。现代技术。其中，谓词抽象是现代模型检测中广泛使用的一种重要技术。这种技术已被证明，以提高在无限状态系统的可达性计算技术的有效性。在这种技术中，一个无限状态系统抽象地表示为一个有限状态系统，其中抽象模型的状态对应于一组选定的原子谓词的真值。谓词抽象在（8）中首次引入，作为自动确定无限状态系统的不变性质的方法。这种技术涉及使用一组称为谓词的公式来抽象具体的转换系统，这些谓词通常表示具体系统的一些状态属性。谓词抽象的实用性受到两个问题的阻碍。首先，需要手动提供谓词（11，7）。这意味着选择适当的抽象谓词是基于用户驱动的试错过程。高度的用户干预也阻碍了与实际软件开发过程的无缝集成。第二，为了验证相关的系统属性，通常抽象过于粗糙。这需要抽象细化（6），通常遵循反例指导的抽象细化方案（5，3）。真实的时间模型是具有大状态空间的系统的一个示例，因为时间给系统增加了很多复杂性。在这种情况下，最近已经有越来越多的研究提供了一种手段，这种模型的抽象。本文的目的是根据（1）的时间自动机模型，为并发密集实时模型的自动谓词抽象技术提供支持。我们提出了一种方法来生成一组有效的预测比手动，特设的过程将能够提供。我们使用我们最近的工作（2）的结果来分析验证下的系统的行为，以发现其局部状态不变，并删除永远不能遍历的转换。然后，我们描述了一种方法来计算这些状态不变量的基础上的谓词抽象。我们使用有关控制状态标签的信息，以及新计算的不变量在考虑控制状态时，确定的抽象谓词。我们开发了一个原型
Introduction Model checking has been widely successful in validating and debugging hardware de- signs and communication protocols. However, state-space explosion is an intrinsic problem which limits the applicability of model checking tools. To overcome this limitation software model checkers have suggested different approaches, among which abstraction methods have been highly esteemed. modern techniques. Among others, predicate abstraction is a prominent technique which has been widely used in modern model checking. This technique has been shown to enhance the effectiveness of the reachability computation technique in infinite-state systems. In this te chnique an infinite-state system is represented abstractly by a finite-state system, where states of the abst ract model correspond to the truth valuations of a chosen set of atomic predicates. Predicate abstraction was first introduced in (8) as a method for auto- matically determining invariant properties of infinite-st ate systems. This technique involves abstracting a concrete transition system using a set of formulas called predicates which usually denote some state properties of the concrete system. The practical applicability of predicate abstraction is im peded by two problems. First, predicates need to be provided manually (11, 7). This means that the selection of appropriate abstraction predicates is based on a user-driven trial-and-error process. The high degree of user intervention also stands in the way of a seamless integration into practical software development processes. Second, very often the abstraction is too coarse in order to allow relevant system properties to be verified. This calls for abstrac- tion refinement (6), often following a counterexample guide d abstraction refinement scheme (5, 3). Real time models are one example of systems with a large state space as time adds much complexity to the system. In this event, recently there have been increasing number of research to provide a means for the abstraction of such models. It is the objective of this paper to provide support for an automated predicate abstraction technique for concurrent dense real-time models according to the timed automaton model of (1). We propose a method to generate an efficient set of pred icates than a manual, ad-hoc process would be able to provide. We use the results from our recent work (2) to analyze the behavior of the system under verification to discover its local state invari ants and to remove transitions that can never be traversed. We then describe a method to compute a predicate abstraction based on these state invariants. We use information regarding the control state labels as well as the newly computed invariants in the considered control states when determining the abstraction predicates. We have developed a prototype