23 Mar, 2012
4 Oct, 2006
24 May, 2005:
tvt.BBreduction:
Finds a minimal LSTS wrt. branching bisimulation equivalence. The
equivalence is sensitive to divergences and differentiates between
deadlocks and divergences. The algorithm used is an adaptation of
Groote & Vaandrager: "An Efficient Algorithm for Branching Bisimulation
and Stuttering Equivalence".tvt.unfold:
A new efficient unfolding operator and compiler for the TVT input language.
22 March, 2004:
tvt.extendedrules and to tvt.illux. Also, a
little bug in tvt.parallel fixed. The bug produced results
bigger than necessary when stubborn sets were used.20 May, 2003:
tvt.CFFDcompare sh script, an erroneous handling of livelock
reject proposition in tvt.parallel and a bug in handling of
promises in LSTS files.21 February, 2003:
TVT --Tampere Verification Tool-- is a toolset for error detection and automatic verification of concurrent and reactive systems. One of the key features of TVT is the support for both action and state based verification. This is made possible by the labelled state transition system (LSTS), the formal model used in TVT. LSTS is used to represent either the behaviour of a complete system or the behaviour of a component of a system.
TVT provides tools for advanced state space methods, and a framework for further tool development. It is published under the NOKOS open source license to welcome third parties in future development. The current version 3.0.1 has been built in the years 1999-2004.
For more information about theoretical concepts, see VARG homepage.
For information about the license agreement, see http://www.opensource.org/licenses/nokia.html.
TVT was originally built for Nokia Research Centre and the development work was mainly done at Tampere University of Technology (TUT for short) Institute of Software Systems and within the institute by the Verification Algorithm Research Group. The work continues for now at TUT.
The presentation slides of TVT Release day, November 12. 2001, Helsinki:
We encourage others to join in the development of TVT and any tools and other additions to it.
TVT is published under the NOKOS license. Please read the license before downloading.