TAILIEUCHUNG - 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 .

• Kĩ thuật Viễn thông
• Hệ thống thời gian
• thời gian thực
• phân tích thời gian
• xác minh thời gian
• phân phối hệ thống
• Nguyên lý hệ điều hành
• Hệ thời gian thực
• Hệ điều hành thời gian thực
• Kỹ thuật lập trình thời gian thực
• Thiết kế ứng dụng thời gian thực
• Ứng dụng thời gian thực
• Hệ thống thời gian thực hành
• Dự án làm xe tự hành
• Xe tự hành
• Cấu tạo một hệ thống thời gian thực
• Bài giảng Hệ thống thông tin công nghiệp
• Hệ thống thông tin công nghiệp
• Mạng truyền thông công nghiệp
• Vấn đề thời gian thực
• Xử lý thời gian thực
• Bài giảng Xử lý số tín hiệu
• Xử lý số tín hiệu
• Hệ thống thời gian rời rạc
• Hệ thống rời rạc thời gian
• Hệ thống tuyến tính
• Hệ thống bất biến
• Kết hợp lựa chọn Ăng ten phát
• Mã không gian thời gian phân tán
• Hệ thống vô tuyến chuyển tiếp MIMO
• Kỹ thuật chọn lọc ăng ten phát
• Mạng chuyển tiếp vô tuyến
• Lựa chọn ăng ten phát
• Mã không gian thời gian
• hệ thống thời gian thực
• ứng dụng thời gian
• nhiệm vụ độc lập
• nhiệm vụ phụ thuộc