Specifying Message Passing and Time-Critical Systems with Temporal Logic

This monograph is concerned with the application of temporal
logic to the areas of message passing and time-critical
systems. Apart from the practicaluse of temporal logic for
these two application domains, the book also incorporates
pure fundamental studies on temporal logic.
The motivation to study message passing and time critical
systems stems from their importance in practice. Message
passing is one of the most important means of interprocess
communication in distributed systems, either on a high
level, as in telecommunications applications, or on a lower
level, as in implementations of languages like Ada. As for
time-critical systems, among the growing number of real-time
applications there are some highly critical systems such as
computer controlled chemical plants and nuclear power
stations.
The monograph shows how standard temporal logic can be used
for the specification of message passing systems, and
develops a special temporal logic for reasoning about
quantitative temporal properties.The main application area
is that of distributed real-time systems.