An Introduction to Practical Formal Methods using Temporal Logic

Michael Fisher

• Book
• Corrections
• Examples
• Systems
• Slides
• Videos

Book

The Wiley web page for the book is here.

If you notice any mistakes, either in the book or in these pages, please email me.

Thank you.

Corrections

Thanks to all those who have pointed our errors in the book:

• Page 273, Example A.3, missing negation.

  Should be

  ''A OR B is equivalent to NOT ((NOT A) AND (NOT B))''

  Thanks to Ed Briggs for spotting this.

Examples

An ongoing project -- to populate this section with examples.

Systems

• TSPASS: was developed by Michel Ludwig and is available here. A copy of the sources and binaries for version 0.94 of TSPASS is also available here.

• Spin: was developed at Bell Labs primarily by Gerard Holzmann and is freely available for general use from here.

• Concurrent MetateM: this Java implementation was developed by Anthony Hepple and is available here.

  A copy of the zip file for version 0.2.1 is also available here. When unzipped, this file provides the Concurrent MetateM interpreter (an archive of Java class files), documentation and a series of example agent systems.

Slides

Slides (in pdf form) are available below.

1. Temporal Logic

   	ORIGINALS	NEW STYLE
   introduction:	pdf; 4up-pdf	pdf; 4up-pdf
   intuition:	pdf; 4up-pdf	pdf; 4up-pdf
   semantics:	pdf; 4up-pdf	pdf; 4up-pdf
   esoterica:	pdf; 4up-pdf	pdf; 4up-pdf

2. Temporal Specification

   programs:	pdf; 4up-pdf.
   semantics:	pdf; 4up-pdf.
   concurrency:	pdf; 4up-pdf.
   communication:	pdf; 4up-pdf.
   case studies:	pdf; 4up-pdf.
   exercises:	pdf; 4up-pdf.
   esoterica:	pdf; 4up-pdf.

3. Temporal Resolution

   resolution:	pdf; 4up-pdf.
   normal form:	pdf; 4up-pdf.
   loop search:	pdf; 4up-pdf.
   simplification:	pdf; 4up-pdf.
   TSPASS:	pdf; 4up-pdf.

4. Model Checking -- not yet available.

5. Executable Temporal Specification -- not yet available.

   implementation:	pdf; 4up-pdf.
   METATEM:	pdf; 4up-pdf.
   Concurrent METATEM:	implementing the METATEM approach, bringing in deliberation, concurrency, and multi-agent systems
   Advanced:

Videos

An ongoing project -- to populate this page with videos.

About this document ...

An Introduction to Practical Formal Methods using Temporal Logic

This document was generated using the LaTeX2HTML translator Version 2002-2-1 (1.71)

Copyright © 1993, 1994, 1995, 1996, Nikos Drakos, Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999, Ross Moore, Mathematics Department, Macquarie University, Sydney.

The command line arguments were:
latex2html -no_subdir -no_navigation -split 1 -address MFisher@liverpool.ac.uk -t 'Michael Fisher: An Introduction to Practical Formal Methods using Temporal Logic' index.tex

The translation was initiated by Michael Fisher on 2015-01-30