Functional specification of time-sensitive communicating systems

Abstract
A formal model and a logical framework for the functional specification of time-sensitive communicating systems and their interacting components are 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.