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.illux. Also, a little bug in
tvt.parallelfixed. The bug produced results bigger than necessary when stubborn sets were used.
20 May, 2003:
tvt.CFFDcomparesh script, an erroneous handling of livelock reject proposition in
tvt.paralleland 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.