Functional specification of time sensitive communicating systems.pdf

acmSEM 4/25/95 FUNCTIONAL SPECIFICATION OF TIME SENSITIVE COMMUNICATING SYSTEMS1 Manfred Broy Institut für Informatik Technische Universität München Postfach 20 24 20, D-8000 München 2, Germany Abstract A formal model and a logical framework for the functional specification of time sensitive communicating systems and their interacting components is outlined. The specification method is modular with respect to sequential composition, parallel composition, and communication feedback. Nondeterminism is included by underspecification. The application of the specification method to timed communicating functions is demonstrated. Abstractions from time are studied. In particular a rational is given for the chosen concepts of the functional specification technique. The relationship between system models based on nondeterminism and system models based on explicit time notions is investigated. Forms of reasoning are considered. The alternating bit protocol is used as a running example. 1This work was supported by the ESPRIT BASIC RESEARCH ACTION DEMON and by the Sonderforschungs- bereich 342 Werkzeuge und Methoden für die Nutzung paralleler Architekturen 2 1. Introduction The behaviour of distributed systems that communicate by exchanging messages can be represented by functional models. By such a modelling, systems that operate embedded into some environment are described by functions that map histories of input communicat