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

ANALYSIS AND VERIFICATION OF NON-REAL-TIME SYSTEMS A great collection of techniques and tools are available for the reasoning, analysis, and verification of non-real-time systems. This chapter explores the basic foundations of these techniques that include symbolic logic, automata, formal languages, and state transition systems. Many analysis and verification techniques for real-time systems are based on these untimed approaches, as we will see in later chapters. | Real-Time Systems Scheduling Analysis and Verification. Albert M. K. Cheng Copyright 2002 John Wiley Sons Inc. ISBN 0-471-18406-3 CHAPTER 2 ANALYSIS AND VERIFICATION OF NON-REAL-TIME SYSTEMS A great collection of techniques and tools are available for the reasoning analysis and verification of non-real-time systems. This chapter explores the basic foundations of these techniques that include symbolic logic automata formal languages and state transition systems. Many analysis and verification techniques for real-time systems are based on these untimed approaches as we will see in later chapters. Here we give a condensed introduction to some of these untimed approaches without providing mathematically involved proofs and describe their applications to untimed versions of several simple real-time systems. SYMBOLIC LOGIC Symbolic logic is a collection of languages that use symbols to represent facts events and actions and provide rules to symbolize reasoning. Given the specification of a system and a collection of desirable properties both written in logic formulas we can attempt to prove that these desirable properties are logical consequences of the specification. In this section we introduce the propositional logic also called propositional calculus zero-order logic digital logic or Boolean logic the most simple symbolic logic the predicate logic also called predicate calculus or first-order logic and several proof techniques. Propositional Logic Using propositional logic we can write declarative sentences called propositions that can be either true denoted by T or false denoted by F but not both. We use an uppercase letter or a string of uppercase letters to denote a proposition. 10 SYMBOLIC LOGIC 11 Example P denotes car brake pedal is pressed Q denotes car stops within five seconds R denotes car avoids a collision These symbols P Q and R used to represent propositions are called atomic formulas or simply atoms. To express more complex propositions such

• 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