共查询到10条相似文献,搜索用时 46 毫秒
1.
Klaus Havelund Willem Visser 《International Journal on Software Tools for Technology Transfer (STTT)》2002,4(1):8-20
This paper introduces a special section of the STTT journal containing a selection of papers that were presented at the 7th
international SPIN workshop, Stanford, 30 August – 1 September 2000. The workshop was named SPIN Model Checking and Software
Verification, with an emphasis on model checking of programs. The paper outlines the motivation for stressing software verification,
rather than only design and model verification, by presenting the work done in the Automated Software Engineering group at
NASA Ames Research Center within the last 5 years. This includes work in software model checking, testing like technologies
and static analysis.
Published online: 2 October 2002 相似文献
2.
3.
Constraint-based deductive model checking 总被引:2,自引:0,他引:2
Giorgio Delzanno Andreas Podelski 《International Journal on Software Tools for Technology Transfer (STTT)》2001,3(3):250-270
We show that constraint logic programming (CLP) can serve as a conceptual basis and as a practical implementation platform
for the model checking of infinite-state systems. CLP programs are logical formulas (built up from constraints) that have
both a logical interpretation and an operational semantics. Our contributions are: (1) a translation of concurrent systems
(imperative programs) into CLP programs with the same operational semantics; and (2) a deductive method for verifying safety
and liveness properties of the systems which is based on the logical interpretation of the CLP programs produced by the translation.
We have implemented the method in a CLP system and verified well-known examples of infinite-state programs over integers,
using linear constraints here as opposed to Presburger arithmetic as in previous solutions.
Published online: 18 July 2001 相似文献
4.
Carl Pixley Vigyan Singhal 《International Journal on Software Tools for Technology Transfer (STTT)》1999,2(3):288-306
Current practices in the verification of commercial hardware designs (digital, synchronous, and sequential semiconductors)
are described. Recent advances in verification by the mathematical technique called model checking are described, and requirements
for the successful application of model checking in commercial design are discussed. 相似文献
5.
Local model checking and protocol analysis 总被引:2,自引:1,他引:1
Xiaoqun Du Scott A. Smolka Rance Cleaveland 《International Journal on Software Tools for Technology Transfer (STTT)》1999,2(3):219-241
This paper describes a local model-checking algorithm for the alternation-free fragment of the modal mu-calculus that has
been implemented in the Concurrency Factory and discusses its application to the analysis of a real-time communications protocol.
The protocol considered is RETHER, a software-based, real-time Ethernet protocol developed at SUNY at Stony Brook. Its purpose is to provide guaranteed bandwidth
and deterministic, periodic network access to multimedia applications over commodity Ethernet hardware. Our model-checking
results show that (for a particular network configuration) RETHER makes good on its bandwidth guarantees to real-time nodes without exposing non-real-time nodes to the possibility of starvation.
Our data also indicate that, in many cases, the state-exploration overhead of the local model checker is significantly smaller
than the total amount that would result from a global analysis of the protocol. In the course of specifying and verifying
RETHER, we also identified an alternative design of the protocol that warranted further study due to its potentially smaller run-time
overhead in servicing requests for data transmission. Again, using local model checking, we showed that this alternative design
also possesses the properties of interest. This observation points out one of the often-overlooked benefits of formal verification:
by forcing designers to understand their designs rigorously and abstractly, these techniques often enable the designers to
uncover interesting design alternatives. 相似文献
6.
Scott D. Stoller 《International Journal on Software Tools for Technology Transfer (STTT)》2002,4(1):71-91
State-space exploration is a powerful technique for verification of concurrent software systems. Applying it to software systems
written in standard programming languages requires powerful abstractions (of data) and reductions (of atomicity), which focus
on simplifying the data and control, respectively, by aggregation. We propose a reduction that exploits a common pattern of
synchronization, namely, the use of locks to protect shared data structures. This pattern of synchronization is particularly
common in concurrent Java programs, because Java provides built-in locks. We describe the design of a new tool for state-less
state-space exploration of Java programs that incorporates this reduction. We also describe an implementation of the reduction
in Java PathFinder, a more traditional state-space exploration tool for Java programs.
Published online: 2 October 2002
RID="*"
ID="*"Present address: Computer Science Dept., SUNY at Stony Brook, Stony Brook, NY 11794-4400, USA. The author gratefully
acknowledges the support of ONR under Grants N00014-99-1-0358 and N00014-01-1-0109 and the support of NSF under Grant CCR-9876058. 相似文献
7.
Orna Kupferman Moshe Y. Vardi 《International Journal on Software Tools for Technology Transfer (STTT)》2003,4(2):224-233
One of the advantages of temporal-logic model-checking tools is their ability to accompany a negative answer to the correctness
query by a counterexample to the satisfaction of the specification in the system. On the other hand, when the answer to the
correctness query is positive, most model-checking tools provide no witness for the satisfaction of the specification. In
the last few years there has been growing awareness as to the importance of suspecting the system or the specification of
containing an error also in the case model checking succeeds. The main justification of such suspects are possible errors
in the modeling of the system or of the specification. Many such errors can be detected by further automatic reasoning about
the system and the environment. In particular, Beer et al. described a method for the detection of vacuous satisfaction of
temporal logic specifications and the generation of interesting witnesses for the satisfaction of specifications. For example,
verifying a system with respect to the specification ϕ=AG(reqAFgrant) (“every request is eventually followed by a grant”), we say that ϕ is satisfied vacuously in systems in which requests are
never sent. An interesting witness for the satisfaction of ϕ is then a computation that satisfies ϕ and contains a request.
Beer et al. considered only specifications of a limited fragment of ACTL, and with a restricted interpretation of vacuity.
In this paper we present a general method for detection of vacuity and generation of interesting witnesses for specifications
in CTL*. Our definition of vacuity is stronger, in the sense that we check whether all the subformulas of the specification affect
its truth value in the system. In addition, we study the advantages and disadvantages of alternative definitions of vacuity,
study the problem of generating linear witnesses and counterexamples for branching temporal logic specifications, and analyze
the complexity of the problem.
Published online: 22 January 2002 相似文献
8.
Cormac Flanagan 《Science of Computer Programming》2004,50(1-3):253-270
This paper proposes the use of constraint logic to perform model checking of imperative, infinite-state programs. We present a semantics-preserving translation from an imperative language with recursive procedures and heap-allocated mutable data structures into constraint logic. The constraint logic formulation provides a clean way to reason about the behavior and correctness of the original program. In addition, it enables the use of existing constraint logic implementations to perform bounded software model checking, using a combination of symbolic reasoning and explicit path exploration. 相似文献
9.
Symmetric Spin 总被引:1,自引:0,他引:1
Dragan Bošnački Dennis Dams Leszek Holenderski 《International Journal on Software Tools for Technology Transfer (STTT)》2002,4(1):92-106
10.
Henrik Reif Andersen Jorn Lind-Nielsen 《International Journal on Software Tools for Technology Transfer (STTT)》1999,2(3):242-259
Partial model checking is a technique for verifying concurrent systems. It gradually reduces the verification problem to the
final answer by removing concurrent components one-by-one, transforming and minimizing the specifications as it proceeds.
This paper gives a survey of the theory behind partial model checking and the results obtained with it. 相似文献