Accession Number:

ADA326062

Title:

An Interleaving Model for Real Time,

Descriptive Note:

Corporate Author:

STANFORD UNIV CA DEPT OF COMPUTER SCIENCE

Personal Author(s):

• Henzinger, Thomas A.
• Manna, Zohar
• Pnueli, Amir

Report Date:

1990-09-12

Pagination or Media Count:

38.0

Abstract:

The interleaving model is both adequate and sufficiently abstract to allow for the practical specification and verification of many properties of concurrent systems. We incorporate real time into this model by defining the abstract notion of a real-time transition system as a conservative extension of traditional transition systems qualitative fairness requirements are replaced and superseded by quantitative lower-bound and upper-bound real-time requirements for transitions. We present proof rules to establish lower and upper real-time bounds for response properties of real-time transition systems. This proof system can be used to verify bounded-invariance and bounded-response properties, such as timely termination of shared-variables multi-process systems, whose semantics is defined in terms of real-time transition systems.

Descriptors:

• *CONCURRENT ENGINEERING
• *SYSTEMS ANALYSIS
• MATHEMATICAL MODELS
• ALGORITHMS
• COMPUTER COMMUNICATIONS
• REAL TIME
• LINEAR PROGRAMMING
• CONTROL SEQUENCES

Subject Categories:

• Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE