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