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 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. Keywords: Formal specification; Formal verification; Assertional reasoning, Possibilities mappings; Timed automata; I/O automata.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 01, 1989
- Accession Number
- ADA213967
Entities
People
- Hagit Attiya
- Nancy Lynch
Organizations
- Massachusetts Institute of Technology