O'Reilly logo

An Introduction to Practical Formal Methods using Temporal Logic by Michael Fisher

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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 ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required