Authors/Contributors

J. F. Peters III

Document Type

Report

Date

11-1991

Embargo Period

5-2-2012

Keywords

Automata, Design Methodology, Constructive Type Theory, Program specification, Real-Time systems, Temporal Logic, Visualization. CR Categories: C.3, D.1.7, D.2.10, J.7, F.1.1, F.3.1.

Language

English

Disciplines

Computer Sciences

Description/Abstract

A new class of communicating automata called typed Timed lnput/Output Automata (tTAi/os) is introduced. A tTAi/o is a predicate automaton used for specifying and reasoning about real-time systems. The typing discipline suggested for predicate automata is in the tradition of Martin-Löf's constructive type theory. A type A is a proposition, which is defined when a prescription for constructing a proof of A is given. A fragment of Girard's linear logic is used in classifying state types. An illustration of the use of tTAi/os in specifying a light-controller is presented. An abstract program is extracted during a proof of an automaton specification. To illustrate the methodology in constructive reasoning about a tTAi/o, a proof which derives a partial abstract program is given.

Additional Information

School of Computer and Information Science, Syracuse University, SU-CIS-91-23

Source

local

Share

COinS
 
 

To view the content in your browser, please download Adobe Reader or, alternately,
you may Download the file to your hard drive.

NOTE: The latest versions of Adobe Reader do not support viewing PDF files within Firefox on Mac OS and if you are using a modern (Intel) Mac, there is no official plugin for viewing PDF files within the browser window.