Using Mappings to Prove Timing Properties
MASSACHUSETTS INST OF TECH CAMBRIDGE LAB FOR COMPUTER SCIENCE
Pagination or Media Count:
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 variant 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.
- Computer Programming and Software