CaltechAUTHORS
  A Caltech Library Service

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

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

This is the latest version of this item.

[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:20150324-144547664

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)
Subject Keywords:formal verification, finite automata, omega automata, linear temporal logic, LTL, logic model checking
Record Number:CaltechAUTHORS:20150324-144547664
Persistent URL:http://resolver.caltech.edu/CaltechAUTHORS:20150324-144547664
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:56038
Collection:CaltechAUTHORS
Deposited By: Gerard Holzmann
Deposited On:24 Mar 2015 23:03
Last Modified:22 Jul 2015 19:27

Available Versions of this Item

Repository Staff Only: item control page