Accession Number:

ADA218136

Title:

Using Mappings to Prove Timing Properties

Descriptive Note:

Technical rept.

Corporate Author:

MASSACHUSETTS INST OF TECH CAMBRIDGE LAB FOR COMPUTER SCIENCE

Personal Author(s):

Report Date:

1989-12-16

Pagination or Media Count:

49.0

Abstract:

A new technique for proving timing properties for timing-based algorithms is described it is an extension of the mapping techniques previously used in proofs of safety properties for asynchronous concurrent systems. The key to the method is a way of representing a system with timing constraints as an automaton whose state includes predictive timing information. Timing assumptions and timing requirements for the system are both represented in this way. A multivalued mapping from the assumptions automation to the requirements automation is then used to show that the given system satisfies the requirements. The technique is illustrated with two simple examples, a resource manager and a signal relay. The technique is shown to be complete, that is, if some automaton with certain timing assumptions has certain timing behavior, the there exists a mapping from the assumptions automation to the requirements automation.

Subject Categories:

  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE