Using Mappings to Prove Timing Properties
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 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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Mar 05, 1991
- Accession Number
- ADA234404
Entities
People
- Hagit Attiya
- Nancy Lynch
Organizations
- Massachusetts Institute of Technology