Model Cheking,10.1007/BFb0058022,Edmund M. Clarke

Model Cheking   (Citations: 4031)
BibTex | RIS | RefWorks Download
Model checking is an automatic technique for verifying finite-state reactive systems, such as sequential circuit designs and communication protocols. Specifications are expressed in temporal logic, and the reactive system is modeled as a statetransition graph. An efficient search procedure is used to determine whether or not the state-transition graph satisfies the specifications. We describe the basic model checking algorithm and show how it can be used with binary decision diagrams to verify properties of large state-transition graphs. We illustrate the power of model checking to find subtle errors by verifying part of the Contingency Guidance Requirements for the Space Shuttle.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ... of nite state machines [20], asks the following question: given a (control ow) graph over a set of nodes and edges, an initial state, and an error state, does there exist a path from the initial to the error state? Subsequent to the recognition that a large class of computer systems can be modeled as nite state machines, this problem received a lot of attention from researchers interested in formal verication of computer systems [19, 7]. ...

    Akash Lalet al. Corral: A Solver for Reachability Modulo Theories

    • ...We refer to [12] for detailed background on LTL, automata and model checking.,See [12] for a detailed description of the syntax and semantics of CTL.,Finally we note that all the algorithms of this section apply also to the more powerful branching time logic CTL* (see [12] for a definition) with exactly the same complexity:...

    Patrice Godefroidet al. Analysis of Boolean Programs

    • ...Other interesting directions are extensions of this approach to branching time logical specifications, such as computation tree logic specifications (Clarke 1997), and to more complicated dynamics, such as polynomial dynamics (Benedetto 2002)...

    Yajuan Sunet al. An input–output simulation approach to controlling multi-affine system...

    • ...Temporal logics (LTL, CTL and CTL*) were initially intended as a framework for specifying and verifying the correctness of digital circuits and computer programs [1]...
    • ...Rich, human-like specifications can be obtained by interconnecting these operators, and details on syntax, semantics, and usage of LTL X in connection with continuous systems can be found in [1], [2], [4]...

    Narcis Ghitaet al. Probabilistic car-like robot path planning from temporal logic specifi...

    • ...It aims to be a lightweight verification technique complementing other verification techniques such as model checking [2] and testing [3]...
    • ...• ⊲alive ∈ [0,2]Udone states that the event done has to occur eventually and that until then, the eventalive must occur every 2 time units...
    • ...• ⊲alive ∈ [0,2]Udone evaluates to ? if done has not occurred so far while two subsequent occurrences of alive have never been separated by more than 2 time units...

    Andreas Baueret al. Runtime Verification for LTL and TLTL

Sort by: