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