tailieunhanh - Thời gian thực - hệ thống P4

MODEL CHECKING OF FINITE-STATE SYSTEMS One way to show that a program or system meets the designer’s specification is to manually construct a proof using axioms and inference rules in a deductive system such as temporal logic, a first-order logic capable of expressing relative ordering of events. This traditional, manual approach to concurrent program verification is tedious and error-prone even for small programs. For finite-state concurrent systems and systems that can be represented as such, we can use model checking instead of proof construction to check their correctness relative to their specifications | Real-Time Systems Scheduling Analysis and Verification. Albert M. K. Cheng Copyright 2002 John Wiley Sons Inc. ISBN 0-471-18406-3 CHAPTER 4 MODEL CHECKING OF FINITE-STATE SYSTEMS One way to show that a program or system meets the designer s specification is to manually construct a proof using axioms and inference rules in a deductive system such as temporal logic a first-order logic capable of expressing relative ordering of events. This traditional manual approach to concurrent program verification is tedious and error-prone even for small programs. For finite-state concurrent systems and systems that can be represented as such we can use model checking instead of proof construction to check their correctness relative to their specifications. In the model checking approach we represent the concurrent system as a finite-state graph which can be viewed as a finite Kripke structure. The specification or safety assertion is expressed in propositional temporal logic formulas. We can then check whether the system meets its specification using an algorithm called a model checker. In other words the model checker determines whether the Kripke structure is a model of the formula s . Several model checkers are available and they vary in code and run-time complexity. Here we describe one of the first model checkers proposed by Clarke Emerson and Sistla 1986 and a more efficient symbolic model checker developed later by Burch et al. 1990a . In Clarke Emerson and Sistla s 1986 approach the system to be checked is represented by a labeled finite-state graph and the specification is written in a propositional branching-time temporal logic called computation tree logic CTL . The use of linear-time temporal logic which can express fairness properties is ruled out since a model checker such as logic has high complexity. Instead fairness requirements are moved into the semantics of CTL. In this chapter we use the terms program and system interchangeably. 86 SYSTEM SPECIFICATION 87 .