ON A FORMALIZATION OF REAL-TIME PROGRAMS.

Wagner Chiepa Cunha, Masafumi Yamashita, Tadashi Ae

Research output: Contribution to journalArticle

Abstract

We propose a new model for real-time programs. A set of concurrent processes executed by a time-shared single processor interacts with a set of input tapes and a set of output tapes representing their environment. Processes access their tapes through reading heads and writing heads. The distinctive feature of our model is the way the movement of heads is controlled. Their movement is not controlled by programs. Instead, they move unidirectionally scanning the tapes according to the flow of time. Stimuli for a process (responses by a process) are modeled as a sequence of symbols, representing data, interspersed with sequences of a special symbol representing time intervals separating successive stimuli (responses). We define important properties of real-time programs including data overrun, deadlock and correctness, and show an example of verification of these properties for a small and typical real-time program.

Original languageEnglish
Pages (from-to)866-876
Number of pages11
JournalTransactions of the Institute of Electronics and Communication Engineers of Japan. Section E
VolumeE69
Issue number8
Publication statusPublished - Aug 1986
Externally publishedYes

Fingerprint

Tapes
Scanning

All Science Journal Classification (ASJC) codes

  • Engineering(all)

Cite this

ON A FORMALIZATION OF REAL-TIME PROGRAMS. / Cunha, Wagner Chiepa; Yamashita, Masafumi; Ae, Tadashi.

In: Transactions of the Institute of Electronics and Communication Engineers of Japan. Section E, Vol. E69, No. 8, 08.1986, p. 866-876.

Research output: Contribution to journalArticle

Cunha, Wagner Chiepa ; Yamashita, Masafumi ; Ae, Tadashi. / ON A FORMALIZATION OF REAL-TIME PROGRAMS. In: Transactions of the Institute of Electronics and Communication Engineers of Japan. Section E. 1986 ; Vol. E69, No. 8. pp. 866-876.
@article{e7e167288eb147618adea612e205254c,
title = "ON A FORMALIZATION OF REAL-TIME PROGRAMS.",
abstract = "We propose a new model for real-time programs. A set of concurrent processes executed by a time-shared single processor interacts with a set of input tapes and a set of output tapes representing their environment. Processes access their tapes through reading heads and writing heads. The distinctive feature of our model is the way the movement of heads is controlled. Their movement is not controlled by programs. Instead, they move unidirectionally scanning the tapes according to the flow of time. Stimuli for a process (responses by a process) are modeled as a sequence of symbols, representing data, interspersed with sequences of a special symbol representing time intervals separating successive stimuli (responses). We define important properties of real-time programs including data overrun, deadlock and correctness, and show an example of verification of these properties for a small and typical real-time program.",
author = "Cunha, {Wagner Chiepa} and Masafumi Yamashita and Tadashi Ae",
year = "1986",
month = "8",
language = "English",
volume = "E69",
pages = "866--876",
journal = "Transactions of the Institute of Electronics and Communication Engineers of Japan. Section E",
issn = "0387-236X",
number = "8",

}

TY - JOUR

T1 - ON A FORMALIZATION OF REAL-TIME PROGRAMS.

AU - Cunha, Wagner Chiepa

AU - Yamashita, Masafumi

AU - Ae, Tadashi

PY - 1986/8

Y1 - 1986/8

N2 - We propose a new model for real-time programs. A set of concurrent processes executed by a time-shared single processor interacts with a set of input tapes and a set of output tapes representing their environment. Processes access their tapes through reading heads and writing heads. The distinctive feature of our model is the way the movement of heads is controlled. Their movement is not controlled by programs. Instead, they move unidirectionally scanning the tapes according to the flow of time. Stimuli for a process (responses by a process) are modeled as a sequence of symbols, representing data, interspersed with sequences of a special symbol representing time intervals separating successive stimuli (responses). We define important properties of real-time programs including data overrun, deadlock and correctness, and show an example of verification of these properties for a small and typical real-time program.

AB - We propose a new model for real-time programs. A set of concurrent processes executed by a time-shared single processor interacts with a set of input tapes and a set of output tapes representing their environment. Processes access their tapes through reading heads and writing heads. The distinctive feature of our model is the way the movement of heads is controlled. Their movement is not controlled by programs. Instead, they move unidirectionally scanning the tapes according to the flow of time. Stimuli for a process (responses by a process) are modeled as a sequence of symbols, representing data, interspersed with sequences of a special symbol representing time intervals separating successive stimuli (responses). We define important properties of real-time programs including data overrun, deadlock and correctness, and show an example of verification of these properties for a small and typical real-time program.

UR - http://www.scopus.com/inward/record.url?scp=0022761874&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0022761874&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:0022761874

VL - E69

SP - 866

EP - 876

JO - Transactions of the Institute of Electronics and Communication Engineers of Japan. Section E

JF - Transactions of the Institute of Electronics and Communication Engineers of Japan. Section E

SN - 0387-236X

IS - 8

ER -