Using mappings to prove timing properties.

*(English)*Zbl 0773.68054Summary: A new technique for proving time 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.

##### MSC:

68Q60 | Specification and verification (program logics, model checking, etc.) |

68Q10 | Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) |

##### Keywords:

assertional reasoning; possibilities mappings; timed automata; I/O automata; progress functions; safety; concurrent algorithms; time properties; timing-based algorithms
PDF
BibTeX
XML
Cite

\textit{N. A. Lynch} and \textit{H. Attiya}, Distrib. Comput. 6, No. 2, 121--139 (1992; Zbl 0773.68054)

Full Text:
DOI

##### References:

[1] | Abadi M, Lamport L: The existence of refinement mappings. DEC SRC Res Rep 29 (1988) · Zbl 0728.68083 |

[2] | Abadi M, Lamport L: An old-fashioned recipe for real time. Proc. REX Workshop ”Real-Time: Theory in Practice”. Mook, The Netherlands 1991 |

[3] | Alur R, Henzinger T: Real-time logics: complexity and expressiveness. Proc 5th IEEE Symp on Logic in Computer Science, pp 390–401 (1990) · Zbl 0791.68103 |

[4] | Alur R, Courcoubetis C, Dill D: Model-checking for real-time systems. Proc 5th IEEE Symp on Logic in Computer Science, 1990 · Zbl 0769.68088 |

[5] | Alur R, Dill D: Automata for modelling real-time systems. Proc ICALP ’90, Lect Notes Comp Sci vol 443: Springer, Berlin Heidelberg New York, pp 322–335 · Zbl 0765.68150 |

[6] | Attiya H, Lynch N: Time bounds of real-time process control in the presence of timing uncertainty. Proc 10th Real-Time Systems Symposium, pp 268–284, December 1989. Expanded version available as Tech Rep MIT/LCS/TR-403, Laboratory for Computer Science, MIT, July 1989 |

[7] | Bernstein A, Harter P Jr: Proving real-time properties of programs with temporal logic. Proc 8th Symp on Operating System Principles. Operating Syst Rev 15 (5):1–11 (1981) · doi:10.1145/1067627.806585 |

[8] | Coolahan JE, Roussopoulus SN: Timing requirements for time-driven systems using augmented Petri nets. IEEE Trans Software Eng SE-9 (5):603–616 (1983) · Zbl 05341703 · doi:10.1109/TSE.1983.235261 |

[9] | Gabrielian A, Franklin MW: State-based specification of complex real-time systems. Proc 9th IEEE Real-Time Systems Symp, pp 2–11 (1988) |

[10] | Hasse VH: Real-time behavior of programs. IEEE Trans Software Eng SE-7 (5):494–501 (1981) · Zbl 05341687 · doi:10.1109/TSE.1981.231111 |

[11] | Harel E, Lichtenstein O, Pnueli A: Explicit clock temporal logic. Proc 5th IEEE Symp on Logic in Computer Science, pp 402–413 (1990) |

[12] | Henzinger TA, Manna Z, Pnueli A: Temporal proof methodologies for real-time systems. Proc ACM Symp on Principles of Programming Languages, pp 353–366 (1991) |

[13] | Hooman J: A compositional proof theory for real-time distributed message passing. TR 4-1-1(1), Department of Mathematics and Computer Science, Eindhoven University of Technology 1987 · Zbl 0615.68024 |

[14] | Jahanian F, Mok A: A graph-theoretic approach for timing analysis and its implementation. IEEE Trans Comput C-36 (8):961–975 (1987) · Zbl 0618.68008 · doi:10.1109/TC.1987.5009519 |

[15] | Jahanian F, Stuart DA: A method for verifying properties of modechart specifications. Proc 9th IEEE Real-Time Systems Symp, pp 12–21 (1988) |

[16] | Koymans R, Vytopil J, deRoever WP: Real-time programming and asynchronous message passing. Proc 2nd ACM Symp on Principles of Distrib Comput, pp 187–197 (1983) |

[17] | Lamport L: Specifying concurrent program modules. ACM Trans Program Lang Syst. 5 (2):190–222 (1983) · Zbl 0516.68010 · doi:10.1145/69624.357207 |

[18] | Lamport L, Abadi M: Refining and composing real-time specifications (in progress) |

[19] | Lewis HR: Finite-state analysis of asynchronous circuits with bounded temporal uncertainty. Tech Rep TR-15-89, Aiken Computation Laboratory, Harvard University |

[20] | Lynch N, Harvey A, Perlman R, Varghese G: An analysis of the OSI network layer link state packet distribution protocol (in progress) |

[21] | Lynch N: Concurrency control for resilient nested transactions. Adv Comput Res 3:335–373 (1986) |

[22] | Lynch N, Attiya H: Using mappings to prove timing properties. Technical Memo MIT/LCS/TM-412.b, Laboratory for Computer Science, MIT, March 1990 · Zbl 0773.68054 |

[23] | Lynch N, Attiya H: Using mappings to prove timing properties. Proc of the 9th Annu ACM Symp on Principles of Distributed Computing, Quebec, Canada, pp 265–280 (1990) · Zbl 0773.68054 |

[24] | Lynch N, Goldman K: Lecture notes for 6.852. MIT/LCS/RSS-5, Laboratory for Computer Science, MIT, 1989 |

[25] | Lynch N, Tuttle M: Hierarchical correctness proofs for distributed algorithms. Proc 7th ACM Symp on Principles of Distributed Computing, pp 137–151 (1987). Expanded version available as Technical Report MIT/LCS/TR-387, Laboratory for Computer Science, MIT, April 1987 |

[26] | Lynch N, Tuttle M: An introduction to input/output automata. CWI-Quarterly, vol 2, no 3, 1989. Also: Technical Memo, MIT/LCS/TM-373, Laboratory for Computer Science Massachusetts Institute of Technology, November 1988 · Zbl 0677.68067 |

[27] | Lynch N, Vaandrager F: Forward and backward simulations for timing-based systems. Proc REX Workshop ”Real-Time: Theory in Practice”, Mook, The Netherlands 1991 |

[28] | Manna Z: Mathematical theory of computation. McGraw-Hill Comput Sci Ser. MacGraw-Hill 1974 |

[29] | Merritt M, Modugno F, Tuttle M: Time constrained automata. In: Baeten JCM, Groote JF (eds) Proc CONCUR 91. Amsterdam, Lect Notes Comput Sci vol 527, Springer, Berlin Heidelberg New York, pp 408–423 |

[30] | Milner R: Calculi for synchrony and asynchrony. TCS 25, pp 267–310 (1983) · Zbl 0512.68026 · doi:10.1016/0304-3975(83)90114-7 |

[31] | Neumann PG, Lamport L: Highly dependable distributed systems. Tech Rep, SRI International, Contract Number DAEA18-81-G-0062, SRI Project 4180, June 1983 |

[32] | Ostroff JS: Deciding properties of timed transion models. IEEE Trans Paral Distrib Sys 1 (2):170–183 (1990) · Zbl 05106644 · doi:10.1109/71.80145 |

[33] | Ostroff JS: Survey of formal methods for the specification and design of real-time systems IEEE Press (to appear) |

[34] | Ostroff JS, Wonham WM: A framework for real-time discrete event control. IEEE Trans Autom Control (1990) · Zbl 0709.68029 |

[35] | Peterson G, Fischer M: Economical solutions for the critical section problem in a distributed system. Proc 9th ACM Symp on Theory of Computing, pp 91–97 (1977) |

[36] | Schneider FB: Real-time reliable systems project. Foundations of Real-Time Computing Research Initiative, ONR Kickoff Workshop, pp 28–32 (1988) |

[37] | Shankar AU, Lam S: Time-dependent distributed systems: proving safety, liveness and timing properties. Distrib Comput 2:61–79 (1987) · doi:10.1007/BF01667079 |

[38] | Shaw AC: Reasoning about time in higher-level language software. IEEE Trans Software Eng SE-15 (7):875–889 (1989) · Zbl 05114092 · doi:10.1109/32.29487 |

[39] | Sifakis J: Petri nets for performance evaluation. Measuring, modeling and evaluating computer systems. In: Beilner H, Gelenbe E (eds) Proc 3rd Symp IFIP Working Group 7.3, Amsterdam, North-Holland 1977, pp 75–93 |

[40] | Stankovic J, Ramamritham K: The SPRING Kernel: a new paradigm for real-time operating systems. ACM Operating Syst Rev 23 (3):54–71 (1989) · Zbl 05445825 · doi:10.1145/71021.71024 |

[41] | Tel G: Assertional verification of a timer based protocol. Proc ICALP ’88, Lect Notes Comput Sci vol 317, Springer, Berlin Hiedelberg New York, pp 600–614 · Zbl 0649.68017 |

[42] | Zwarico A: Timed acceptance: an algebra of time dependent computing, Ph.D. Thesis, Department of Computer and Information Science, University of Pennsylvania 1988 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.