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

Chia sẻ: Va Line Line | Ngày: | Loại File: PDF | Số trang:48

lượt xem

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

Mô tả tài liệu
  Download Vui lòng tải xuống để xem tài liệu đầy đủ

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

Chủ đề:

Nội dung Text: Thời gian thực - hệ thống P4

Đồng bộ tài khoản