| Real-time systems are characterized by stringent timing requirements that they must satisfy. Traditional formalisms that abstract away quantitative properties are inadequate for this type of systems. To model the quantitative properties of real-time applications (e.g., the elapsing of time), a number of extensions have been proposed which allow explicit timing requirements to be specified. In general, these extensions are equipped with a form of delay statement that can capture some kinds of timing requirements; however, timing requirements can be arbitrarily complicated and a simple form of delay statement is often inadequate for specifying these requirements. We extend an existing formalism based on process algebras allowing complex behavior to be modeled, and provide a translation from process algebraic specifications to timed automata by which real-time requirements can be verified using model checking techniques. This research is aimed at developing a methodology based on two well-known formal methods for real-time systems, timed process algebra and temporal logic, by combining their strengths--the expressive power, applicability and comprehensibility of timed process algebra and the verification power of temporal logic.; Timed process algebras, one of the most commonly used frameworks for specifying and reasoning about real-time systems, allow complex structural properties to be modeled by means of structural operators, e.g., prefix, nondeterministic choice, and parallel composition; many interesting real-time requirements can be expressed by the introduction of timed operators, e.g., time delays, timeout, and watchdog. However, periodic behavior, a very common feature in real-time systems, cannot be modeled easily by any existing process algebras, such as Timed CSP, Timed CCS, and Algebra of Timed Processes (ATP). We define an enhanced timed process algebra, called Language of Timed Processes (LTP). LTP extends ATP with a new exact operator that captures directly the behavior of periodic processes. The operational semantics of LTP is defined in terms of a labeled transition system.; A distinctive advantage of LTP is that LTP specifications are amenable to automatic verification. To accomplish this goal, we define a set of translation rules that translate a specification into an equivalent timed automaton, and then the temporal properties specified in timed computation tree logic (TCTL) can be verified upon the resulting timed automata. An additional contribution of this work is that I simplify timed automata by detecting and reducing unnecessary clock variables. The resulting models can substantially reduce the verification effort with respect to existing approaches. |
