An Introduction to Practical Formal Methods using Temporal Logic

Michael Fisher

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

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

   introduction:	pdf; 4up-pdf.
   intuition:	pdf; 4up-pdf.
   semantics:	pdf; 4up-pdf.
   esoterica:	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 -- partially available:

   resolution:	pdf; 4up-pdf.
   normal form:	pdf; 4up-pdf.

4. Model Checking -- not yet available.

5. Executable Temporal Specification -- not yet available.

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 2012-01-27