Our group is developing two tools which can be used in computer aided verification

TPAL tool

TPAL is a tool for the verification and simulation of concurrent systems, which are modeled by using a Timed and Probabilistic Process Algebra. The main advantage of TPAL is that we may write the specifications directly by using an algebraic language, and some alternative representation can automatically generated. The current version of TPAL has the following features:

Full support for the creation and edition of specifications and projects in TPAL. Syntax and semantic analysis of TPAL specifications. Generation of Probabilistic-Dynamic State Graphs for TPAL specifications. Simple reduction of the generated graphs. Graph browser, and simulation by using the graphs. Generation of Timed-Arc Petri Nets. Timed-Arc Petri Nets browser, and simulation by using the nets. Translation of Dynamic State Graphs into Time Automata for UPPAAL tool. Configuration of some parameters (graph browser and simulation.)

You can obtain the current linux version HERE.

WST tool

This tool is an integrated environment for translating automatically WS-CDL specifications to Timed Automata. WS-CDL is an XML-based language, and Timed Automata in UPPAAL are represented by another XML file. Thus, the tool applies XSLT stylesheets to a WS-CDL document and obtains an XML document that defines a system in UPPAAL. These XSL stylsheets have been previ-ously created with an XSLT editor. The XML document obtained can be visualized, simulated and verificated with UPPAAL. You can obtain the current version HERE.