LCS Publication Details
Publication Title: USING MAPPINGS TO PROVE TIMING PROPERTIES
Publication Author: Lynch, Nancy
Additional Authors: Attiya, Hagit
LCS Document Number: MIT-LCS-TM-412
Publication Date: 12-1-1989
LCS Group: No Group Specified
Additional URL: No URL Given
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 multi-valued mapping from the "assumptions automaton" to the "requirements automaton" is then used to show that the given system satisfies the requirements. One type of mapping is based on a collection of "progress functions" providing measures of progress toward timing goals. The technique is illustrated with two examples, a simple resource manager and a two-process race system..
To obtain this publication:

To purchase a printed copy of this publication please contact MIT Document Services.