Document Type
Report
Date
7-1991
Keywords
communicating automata, program correctness, program specification, real-time systems, temporal logic
Language
English
Disciplines
Computer Sciences
Description/Abstract
A new class of communicating automata called Temporal Input/Output Automata (TAi/os) is introduced. A TAi/o is a predicate automaton used to specify real-time systems. The specification provided by a TAi/o includes state predicates with proof expressions and abstract program syntax as attributes. An abstract program is extracted during a constructive proof of the specification using the proof expressions. A TAi/o specification also includes hard, real-time constraints on program behavior. The predictability of deterministic, temporally complete TAi/o is investigated. The formulation of real-time system transductions and transduction rules for TAi/os in explicit clock temporal logic is given. An illustration of the use of TAi/os in specifying light-controlled vehicles is presented. To illustrate the methodology in constructive reasoning about a TAi/o, a proof which derives a partial abstract program is given.
Recommended Citation
Peters, J. F. III and Ramanna, S., "Constructing Real-Time Systems from Temporal I/O Automata" (1991). Electrical Engineering and Computer Science - Technical Reports. 110.
https://surface.syr.edu/eecs_techreports/110
Source
local
Additional Information
School of Computer and Information Science, Syracuse University, SU-CIS-91-22