Chapter 1 Introduction to Model Checking

摘要

A computer-assisted method for the analysis of dynamical systems that can be modeled by state-transition systems.
Drawing from research traditions in mathematical logic, programming languages, hardware design, and theoretical computer science, model checking is now widely used for the verification of hardware and software in industry.

计算机辅助验证之例

The only effective way to raise the confidence level of a program significantly is to give a convincing proof of its correctness.

Model Checking Chapter

January 1, 1 · 193 words · One minute · Model Checking

chapters of the book

Each chapter of this handbook is a survey in its own right, and reflects the viewpoint, the notation, and the terminology used by the specialists in the respective research area. The handbook chapters are intended as independent introductions to the state-of-the-art research literature on specific topics rather than as chapters of a monograph.

Introduction to Model Checking

Temporal Logic and Fair Discrete Systems

Modeling for Verification

Automata Theory and Model Checking

Explicit-State Model Checking

Partial-Order Reduction

Binary Decision Diagrams

BDD-Based Symbolic Model Checking

Propositional SAT Solving

SAT-Based Model Checking

Satisfiability Modulo Theories

Compositional Reasoning

Abstraction and Abstraction Refinement

Interpolation and Model Checking

Predicate Abstraction for Program Verification

Combining Model Checking and Data-Flow Analysis

Model Checking Procedural Programs

Model Checking Concurrent Programs

Combining Model Checking and Testing

Combining Model Checking and Deduction

Model Checking Parameterized Systems

Model Checking Security Protocols

Transfer of Model Checking to Industrial Practice

Functional Specification of Hardware via Temporal Logic

Symbolic Trajectory Evaluation

The mu-Calculus and Model Checking

Graph Games and Reactive Synthesis

Model Checking Probabilistic Systems

Model Checking Real-Time Systems

Verification of Hybrid Systems

Symbolic Model Checking in Non-Boolean Domains

Process Algebra and Model Checking

Temporal logics

January 1, 1 · 1082 words · 3 min · Model Checking

时序逻辑和公平离散系统

Temporal Logic and Fair Discrete Systems

摘要

Temporal logics can be classified by their view of the evolution of time as either linear or branching.
In the linear-time view, we see time ranging over a linear total order and executions are sequences of states. When the system has multiple possible executions (due to nondeterminism or reading input) we view them as separate possible evolutions and the system has a set of possible behaviors.