MODELING TIMED BEHAVIOR IN REAL-TIME SYSTEMS WITH TEMPORAL LOGIC

This article presents graphic as well as assertional representations of the timed behavior of a real-time system. It introduces finite, directed, labeled graphs called temporal I/O automata (TA(i/o)) to provide a visual means of modeling system behavior. A real-time system is modeled as a collection of communicating TA(i/o)s. A TA(i/o) is associated with an external clock, which makes it possible to formulate hard, real-time constraints on actions performed by a system. Timing constraints provide control engineers with a means of measuring the responsiveness of a system to its environment. This article suggests how real-time temporal logic can be used to describe system behavior concisely. Temporal specifications provide (1) a means of verifying the correctness of a system design, and (2) a basis for constructing implementations of system designs. The behavior of control systems for autonomous vehicles guided by visual feedback are described graphically with TA(i/o)S and textually with temporal logic formulas. Suggestions on how such control systems can be implemented in distributed Ada are also presented.