Chapter 3
Specification
A man with a watch knows what time it is. A man with two watches is never sure.
—Segal's Law
In this Chapter, we will:
- introduce the idea of using temporal logic to represent simple system behaviours (Section 3.1);
- extend this to provide a temporal semantics for a basic imperative programming language (Section 3.2);
- show how to link temporal descriptions of separate elements, particularly to describe distributed, concurrent, communicating systems (Section 3.3);
- highlight a selection of more advanced work including more complex programming languages, alternative models of concurrency, and general properties of temporal semantics (Section 3.4);
- present a final selection of exercises (Section 3.5), the solutions to which can again be found in Appendix B; and
- provide a brief roadmap of the forthcoming chapters (Section 3.6).
3.1 Describing Simple Behaviours
This chapter concerns temporal specification of behaviours. More specifically, we will mainly address ways of describing the behaviours of programs. But what is the link between a program and a specification given as a temporal formula? The following diagram attempts to capture this relationship. Here, a program can be executed, generating an execution sequence. Execution sequences are again just structures isomorphic to the Natural Numbers, together with a mapping from each point to the set of conditions that are true at that point and, hence, execution sequences can correspond to appropriate temporal ...
