CaltechAUTHORS
  A Caltech Library Service

Tau -- a lightweight tool for specifying and verifying tiny automata models

Holzmann, Gerard Tau -- a lightweight tool for specifying and verifying tiny automata models. [Software] (Unpublished) http://resolver.caltech.edu/CaltechAUTHORS:20150211-111542706

WarningThere is a more recent version of this item available.

[img] Archive (GZIP) (tau tool) - Submitted Version
Creative Commons GNU LGPL (Software).

20Kb

Use this Persistent URL to link to this item: http://resolver.caltech.edu/CaltechAUTHORS:20150211-111542706

Abstract

Tau is a small Tcl/Tk application that can be used to quickly specify and formally verify small automata models (the name 'tau' is short for 'tiny automata') It is used as a teaching aid in CS118, a course on the formal verification of asynchronous software systems using logic model checking. Tau requires the availability of a standard C compiler (e.g., gcc) and a recent version of the Spin model checker (e.g., Version 6.4.3 or later) as background tools.


Item Type:Software
Related URLs:
URLURL TypeDescription
http://spinroot.com/Related ItemSpin model checker (used as a background verification engine)
Contact Email Address:gholzmann@acm.org
Subject Keywords:formal verification, finite automata, omega automata, linear temporal logic, LTL, logic model checking,
Record Number:CaltechAUTHORS:20150211-111542706
Persistent URL:http://resolver.caltech.edu/CaltechAUTHORS:20150211-111542706
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:54720
Collection:CaltechAUTHORS
Deposited By: Gerard Holzmann
Deposited On:11 Feb 2015 21:01
Last Modified:11 Feb 2015 21:01

Available Versions of this Item

Repository Staff Only: item control page