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

VERIFICATION USING TIMED AUTOMATA Finite automata and temporal logics have been used extensively to formally verify qualitative properties of concurrent systems. The properties include deadlock- or livelock-freedom, the eventual occurrence of an event, and the satisfaction of a predicate. The need to reason with absolute time is unnecessary in these applications, whose correctness depends only on the relative ordering of the associated events and actions. These automata-theoretic and temporal logic techniques using finitestate graphs are practical in a variety of verification problems in network protocols, electronic circuits, and concurrent programs | Real-Time Systems Scheduling Analysis and Verification. Albert M. K. Cheng Copyright 2002 John Wiley Sons Inc. ISBN 0-471-18406-3 CHAPTER 7 VERIFICATION USING TIMED AUTOMATA Finite automata and temporal logics have been used extensively to formally verify qualitative properties of concurrent systems. The properties include deadlock- or livelock-freedom the eventual occurrence of an event and the satisfaction of a predicate. The need to reason with absolute time is unnecessary in these applications whose correctness depends only on the relative ordering of the associated events and actions. These automata-theoretic and temporal logic techniques using finite-state graphs are practical in a variety of verification problems in network protocols electronic circuits and concurrent programs. More recently several researchers have extended these techniques to timed or real-time systems while retaining many of the desirable features of their untimed counterparts. In this chapter we present two automata-theoretic techniques based on timed automata. The Lynch-Vaandrager approach Lynch and Vaandrager 1991 Heitmeyer and Lynch 1994 is more general and can handle finite and infinite state systems but it lacks an automatic verification mechanism. Its specification can be difficult to write and understand even for relatively small systems. The Alur-Dill approach Alur Fix and Henzinger 1994 is less ambitious and is based on finite automata but it offers an automated tool for verification of desirable properties. Its dense-time model can handle time values selected from the set of real numbers whereas discrete-time models such as those in Statecharts and Modecharts use only integer time values. LYNCH-VAANDRAGER AUTOMATA-THEORETIC APPROACH Heitmeyer and Lynch 1994 advocate the use of three specifications to formally describe a real-time system. A specification consists of the description of one or more 187 188 VERIFICATION USING TIMED AUTOMATA timed automata. First an axiomatic .

• 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