**排序方式：**共有21条查询结果，搜索用时 31 毫秒

1.

2.

3.

提出一个结合变量抽象和有界模型检测(BMC)的验证框架,用于证明反例不存在或输出存在反例.引入变量极小不可满足(VMU)的数学概念来驱动抽象精化的验证过程.一个VMU公式F的变量集合是保证其不可满足性的一个极小集合.严格证明了VMU驱动的精化满足抽象精化框架中的两个理想性质:有效性和极小性.虽然VMU的判定问题和极小不可满足(MU)一样难,即DP完全的,该案例研究表明,在变量抽象精化过程中,VMU比MU更为有效. 相似文献

4.

针对构件组合的状态爆炸问题,改进了反例引导的抽象精化框架,提出了组合式的抽象精化方法,使构件组合的模型检验转化为各成分构件的局部抽象精化,降低了分析的复杂度.提出了在构件组合情况下基于等价关系和存在商的构件抽象方法,用构件抽象的组合建立构件组合的抽象;提出了组合确认定理并给出证明,使反例确认分解为在各构件上对反例投影的确认;通过对单个构件的等价关系的精化实现构件组合的抽象模型的精化.在模型检验构件组合的过程中,不需要为构件组合建立全局的具体状态空间. 相似文献

5.

Abstractions are important in specifying and proving properties of complex systems. To prove that a given automaton implements an abstract specification automaton, one must first find the correct abstraction relation between the states of the automata, and then show that this relation is preserved by all corresponding action sequences of the two automata. This paper describes tool support based on the PVS theorem prover that can help users accomplish the second task, in other words, in proving a candidate abstraction relation correct. This tool support relies on a clean and uniform technique for defining abstraction properties relating automata that uses library theories for defining abstraction relations and templates for specifying automata and abstraction theorems. The paper then describes how the templates and theories allow development of generic, high level PVS strategies that aid in the mechanization of abstraction proofs. These strategies first set up the standard subgoals for the abstraction proofs and then execute the standard initial proof steps for these subgoals, thus making the process of proving abstraction properties in PVS more automated. With suitable supplementary strategies to implement the “natural” proof steps needed to complete the proofs of any of the standard subgoals remaining to be proved, the abstraction proof strategies can form part of a set of mechanized proof steps that can be used interactively to translate high level proof sketches into PVS proofs. Using timed I/O automata examples taken from the literature, this paper illustrates use of the templates, theories, and strategies described to specify and prove two types of abstraction property: refinement and forward simulation. 相似文献

6.

7.

A new technique is presented to statically check a given procedure against a user-provided property. The method requires no
annotations; it automatically infers a context-dependent specification for each procedure call, so that only as much information
about a procedure is used as is needed to analyze its caller. Specifications are inferred iteratively. Empty specifications
are initially used to over-approximate the effects of all procedure calls; these are later refined in response to spurious
counterexamples. When the analysis terminates, any remaining counterexample is guaranteed to be valid. However, since the
heap is finitized, the absence of a counterexample does not guarantee the validity of the given property in general.

相似文献

Daniel JacksonEmail: |

8.

Chao Wang Roderick Bloem Gary D. Hachtel Kavita Ravi Fabio Somenzi 《Formal Methods in System Design》2006,28(1):5-36

We propose a refinement approach to language emptiness, which is based on the enumeration and the successive refinements of
SCCs on over-approximations of the exact system. Our algorithm is compositional: It performs as much computation as possible
on the abstract systems, and prunes uninteresting part of the search space as early as possible. It decomposes the state space
disjunctively so that each state subset can be checked in isolation to decide language emptiness for the given system. We
prove that the strength of an SCC or a set of SCCs decreases monotonically with composition. This allows us to deploy the
proper model checking algorithms according to the strength of the SCC at hand. We also propose to use the approximate distance
of a fair cycle from the initial states to guide the search. Experimental studies on a set of LTL model checking problems
prove the effectiveness of our method.
This work was done when the first two authors were in University of Colorado at Boulder. Parts of this work appeared in preliminary
form in [38] and [39]. 相似文献

9.

Sagar Chaki Edmund Clarke Joël Ouaknine Natasha Sharygina Nishant Sinha 《Formal Aspects of Computing》2005,17(4):461-483

We present a framework for model checking concurrent software systems which incorporates both states and events. Contrary
to other state/event approaches, our work also integrates two powerful verification techniques, counterexample-guided abstraction
refinement and compositional reasoning. Our specification language is a state/event extension of linear temporal logic, and
allows us to express many properties of software in a concise and intuitive manner. We show how standard automata-theoretic
LTL model checking algorithms can be ported to our framework at no extra cost, enabling us to directly benefit from the large
body of research on efficient LTL verification.
We also present an algorithm to detect deadlocks in concurrent message-passing programs. Deadlock- freedom is not only an
important and desirable property in its own right, but is also a prerequisite for the soundness of our model checking algorithm.
Even though deadlock is inherently non-compositional and is not preserved by classical abstractions, our iterative algorithm
employs both (non-standard) abstractions and compositional reasoning to alleviate the state-space explosion problem. The resulting
framework differs in key respects from other instances of the counterexample-guided abstraction refinement paradigm found
in the literature.
We have implemented this work in the magic verification tool for concurrent C programs and performed tests on a broad set
of benchmarks. Our experiments show that this new approach not only eases the writing of specifications, but also yields important
gains both in space and in time during verification. In certain cases, we even encountered specifications that could not be
verified using traditional pure event-based or state-based approaches, but became tractable within our state/event framework.
We also recorded substantial reductions in time and memory consumption when performing deadlock-freedom checks with our new
abstractions. Finally, we report two bugs (including a deadlock) in the source code of Micro-C/OS versions 2.0 and 2.7, which
we discovered during our experiments.
This research was sponsored by the National Science Foundation (NSF) under grants no. CCR-9803774 and CCR-0121547, the Office
of Naval Research (ONR) and the Naval Research Laboratory (NRL) under contract no. N00014-01-1-0796, the Army Research Office
(ARO) under contract no. DAAD19-01-1-0485, and was conducted as part of the Predictable Assembly from Certifiable Components
(PACC) project at the Software Engineering Institute (SEI).
This article combines and builds upon the papers (CCO

^{+}04) and (CCOS04). Received December 2004 Revised July 2005 Accepted July 2005 by Eerke A. Boiten, John Derrick, Graeme Smith and Ian Hayes 相似文献10.

Bing Li Chao Wang Fabio Somenzi 《International Journal on Software Tools for Technology Transfer (STTT)》2005,7(2):143-155

We present an abstraction refinement algorithm for model checking of safety properties that relies exclusively on a SAT solver for checking the abstract model, testing abstract counterexamples on the concrete model, and refinement. Model checking of the abstractions is based on bounded model checking extended with checks for the existence of simple paths that help in deciding passing properties. All minimum-length spurious counterexamples are eliminated in one refinement step by an incremental procedure that combines the analysis of the conflict dependency graph produced by the SAT solver while looking for concrete counterexamples with an effective refinement minimization procedure. 相似文献