An Introduction to Practical Formal Methods Using Temporal Logic

Michael Fisher

• Publisher: Wiley
• Year: 2011
• Print ISBN: 9780470027882
• eBook ISBN: 9781119991465
• Edition: 1
• Topic: Technology & Engineering
• Subtopic: Electrical Engineering & Telecommunications
• Index: Technology & Engineering

The name "temporal logic" may sound complex and daunting; but while they describe potentially complex scenarios, temporal logics are often based on a few simple, and fundamental, concepts - highlighted in this book. An Introduction to Practical Formal Methods Using Temporal Logic provides an introduction to formal methods based on temporal logic, for developing and testing complex computational systems. These methods are supported by many well-developed tools, techniques and results that can be applied to a wide range of systems.

Fisher begins with a full introduction to the subject, covering the basics of temporal logic and using a variety of examples, exercises and pointers to more advanced work to help clarify and illustrate the topics discussed. He goes on to describe how this logic can be used to specify a variety of computational systems, looking at issues of linking specifications, concurrency, communication and composition ability. He then analyses temporal specification techniques such as deductive verification, algorithmic verification, and direct execution to develop and verify computational systems. The final chapter on case studies analyses the potential problems that can occur in a range of engineering applications in the areas of robotics, railway signalling, hardware design, ubiquitous computing, intelligent agents, and information security, and explains how temporal logic can improve their accuracy and reliability.

• Models temporal notions and uses them to analyze computational systems
• Provides a broad approach to temporal logic across many formal methods - including specification, verification and implementation
• Introduces and explains freely available tools based on temporal logics and shows how these can be applied
• Presents exercises and pointers to further study in each chapter, as well as an accompanying website providing links to additional systems based upon temporal logic as well as additional material related to the book.

Chapter 1

Introduction

Time is an illusion, lunchtime doubly so.

—Douglas Adams

Time plays a central role in our lives. In describing the world, or our activities within it, we naturally invoke temporal descriptions. Some of these are explicit, such as ‘next week’ or ‘in 5 minutes’, while others implicitly acknowledge the passing of time, for example ‘during’, ‘did’ or ‘will do’. Not surprisingly, it is also important to be able to describe temporal aspects within the world of Computer Science: computations naturally proceed through time, and so have a history of activity; computational processes take time to act; some processes must finish before others can start; and so on. Consequently, being able to understand, and reason about, temporal concepts is central to Computer Science.

In this book, we will explain how some of these temporal notions can be described and manipulated. This, in turn, will allow us to carry out a temporal analysis of certain aspects of computation. To be precise in our temporal descriptions, we will use formal logic. These not only provide a concise and unambiguous basis for our descriptions, but are supported by many well-developed tools, techniques and results that we can take advantage of.

This book will provide an introduction to work concerned with formal logic for capturing temporal notions, called temporal logic, together with some of its applications in the formal development and analysis of computational systems. The name ‘temporal logic’ may sound complex and daunting. Indeed, the subject can sometimes be difficult because it essentially aims to capture the notion of time in a logical framework. However, while describing potentially complex scenarios, temporal logic is often based on a few simple, and fundamental, concepts. We aim to highlight these in this book.

As we might expect, this combination of expressive power and conceptual simplicity has led to the use of temporal logic in a range of subjects concerned with computation: Computer Science, Electronic Engineering, Information Systems and Artificial Intelligence. This representation of dynamic activity via temporal formalisms is used in a wide variety of areas within these broad fields, for example Robotics [176, 452], Control Systems [317, 466], Dynamic Databases [62, 110, 467], Program Specification [339, 363], System Verification [34, 122, 285], and Agent-Based Systems [207, 429]. Yet that is not all. Temporal logic also has an important role to play in Philosophy, Linguistics and Mathematics [222, 470], and is beginning to be used in areas as diverse as the Social Sciences and Systems Biology.

But why is temporal logic so useful? And is it really so simple? And how can we use practical tools based on temporal logic? This book aims to (at least begin to) answer these questions.

1.1 Aims of the Book

Our aims here are to

• provide the reader with some of the background to the development and use of temporal logic;
• introduce the foundations (both informal and formal) of a simple temporal logic; and
• describe techniques and tools based on temporal logic and apply them to sample applications.

This book is not deeply technical. It simply aims to provide sufficient introduction to a number of areas surrounding temporal logic to enable either further, in-depth, study or the use of some of the tools described. Consequently, we would expect the readership to consist of those studying Computer Science, Information Systems or Artificial Intelligence at either undergraduate or postgraduate level, or software professionals who wish to expand their knowledge in this area. Since this is an introductory text, we aim to provide references to additional papers, books and online resources that can be used for further, and deeper, study. There are also several excellent, more advanced, textbooks and monographs that provide much greater technical detail concerning some of the aspects we cover, notably [34, 50, 122, 224, 299, 327, 339, 363, 364].

While there are very few proofs in this book, some of the elements are quite complex. In order to support the reader in understanding these aspects, we have often provided both exercises and pointers to further study in each chapter. We have interspersed exercises throughout the text, and sometimes provide a further selection of exercises at the end of each chapter, with answers in Appendix B. In addition, further resources can be found on the Web pages associated with this book:

http://www.csc.liv.ac.uk/∼michael/TLBook

This URL provides links not only to additional material related to the book, but also contains pointers to a range of systems that are, at least in part, based on temporal logic.

1.2 Why Temporal Logic?

As computational systems become more complex, it is often important to be able to describe, clearly and unambiguously, their behaviour. Formal languages with well-defined semantics are increasingly used for this purpose, with formal logic being particularly prominent. This logic not only presents a precise language in which computational properties can be described, but also provides well-developed logical machinery for manipulating and analysing such descriptions.

For example, it is increasingly important to verify that a computational system behaves as required. These requirements can be captured as a formal specification in an appropriately chosen formal logic, with this specification then providing the basis for formal verification. While a system can be tested on many different inputs, formal verification provides a comprehensive approach to potentially establishing the correctness of the system in all possible situations. Verification within formal logic is aided by a logic's machinery, such as proof rules, normal form and decision procedures. Alternatively, we may wish to use the logical specification of a system in other ways, such as treating it as a program and directly executing it. Again, the well-developed logical machinery helps us with this.

Though logical specifications are clearly an important area to develop, the increased complexity of contemporary computational systems has meant that specifications in terms of traditional logic can become inappropriate and cumbersome. Consequently, much of the recent work concerning the use of formal logic in Computer Science has concentrated on developing logic that provides an appropriate level of abstraction for representing complex dynamic properties. It is precisely for this reason that temporal logic has been developed. Temporal logic has been used in Linguistics since the 1960s. In particular, temporal logic was originally used to represent tense in natural language [420]. However, in the late 1970s, temporal logic began to achieve a significant role in the formal specification and verification of concurrent and distributed systems [411, 412]. This logic is now at the heart of many specification, analysis and implementation approaches.

1.2.1 Motivation: Evolution of Computational Systems

The way computational systems are designed and programmed has evolved considerably over the last 40 years. Correspondingly, the abstractions used to characterize such systems have changed during that time. When formal approaches to program development were initially envisaged, the key abstraction was that of a transformational system [260]. Transformational systems are essentially those whose behaviour can be described in terms of each component's input/output behaviour:

In other words, each component in a system receives some input, carries out some operation (typically on data structures), and terminates having produced some output. The...

Table of contents

• Cover
• Title Page
• Copyright
• Preface
• Chapter 1: Introduction
• Chapter 2: Temporal Logic
• Chapter 3: Specification
• Chapter 4: Deduction
• Chapter 5: Model Checking
• Chapter 6: Execution
• Chapter 7: Selected Applications
• Chapter 8: Summary
• Appendix A: Review of Classical Logic
• Appendix B: Solutions to Exercises
• References
• Index