Using mappings to prove timing properties
Nancy Ann Lynch, Hagit Attiya · 1990
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 automaton"to the "requirements automaton" 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 system, and a third, more complex example of a two-process race system.The technique is shown to be complete, that is, if some automaton with certain timing assumptions has certain timing behavior, than there exists a mapping from the "assumptions automaton"to the "requirements automaton".