TranSyT

A tool for the verification of asynchronous concurrent systems 

What is TranSyT

TranSyT is a BDD-based tool specifically designed for the verification of timed and untimed asynchronous concurrent systems. TranSyT system architecture is designed to be modular, open and flexible, such that additional capabilities can be easily integrated. The state of the art CUBDD package is integrated into the system, and the middleware extensions in PDTRAV provide support for complex BDD manipulation strategies.

TranSyT integrates specialized algorithms for untimed reachability analysis based on disjunctive TR partitioning, and relative-time verification for timed systems. Invariant verification for both timed and untimed systems is fully supported, while CTL model checking is currently supported for untimed systems. TranSyT provides orders of magnitude improvement over general untimed verification tools like NuSMV and VIS when applied to concurrent systems, and expands the horizon of timed verification to middle-size real examples.

TranSyT is designed with a precise application field in mind: (1) asynchronous systems, including digital circuits and any type of event-based description formalism; and (2) mixed synchronous-asynchronous systems or synchronous systems with multiple clock domains, like Globally Asynchronous Locally Synchronous (GALS) systems.

System Specification

TSIF (Transition System Interchange Format) is the main input language of TranSyT. TSIF is a low level languaje designed to describe asynchronous event-based systems, although synchronous systems can be also described. The tool can also read Signal Transition Graphs (STG) and circuits in BLIF format through a translation process. An STG is a formal specification of timing diagrams in which the events correspond to rising and falling transitions of control signals. Besides expressing causality, STGs can also specify concurrency and choice. BLIF is a format for circuit description introduced in Berkeley's SIS.

Tool Functionalities

We provide here a high-level overview of the the most relevant features of TranSyT as offered to the user. Details of the architecture and algorithms will be provided in the documentation and related papers.

User Interaction

TranSyT works with an interactive shell, processing systems according to command-line options. The user can activate all phases of the verification process (file parsing, system construction, reachability analysis, model checking, simulation, counter-example generation, etc.) with full control of all available options. Default options are provided, and the user can inspect and modify them as necessary. On top of the interactive shell, a limited but under expansion GUI front-end offers access to all interactive commands, as well as an improved visualization of the systems and the properties under analysis. Visualization of the counter-example traces is also offered via the Graphviz toolkit. Additionally, batch files can also be processed.

System Description

TranSyT can process hierarchical systems formalized (using the TSIF format) as a set of variables to encode the state and events to describe the "actions" that the system can execute, i.e. the state changes that can be executed. Systems can be simultaneously coordinated by variable interchange or event synchronization. Other formalisms can be encoded and easily mapped onto TSIF. Currently we offer a front-end for BLIF and Petri nets, and we are working toward a new SMV front-end.

Reachability Analysis

TranSyT implements specialized reachability schemes based on disjunctive TRs and uses a mixed BFS/DFS traversal that schedules the application of the TR parts in order to maximize the state generation ratio and minimize BDD peaks. These algorithms have demonstrated orders of magnitude improvement over existing BFS / conjunctive TR traversal schemes when applied to asynchronous concurrent systems. State-of-the art conjunctive TR traversal schemes are also available to efficiently manipulate mixed synchronous/asynchronous systems.

Model Checking

TranSyT implements fair CTL model checking, and also offers specialized on-the-fly invariant verification. The tool can be configured to detect
a minimum number of failures in a single traversal. Failing states are stored associated to the verified properties in order to allow selective counter-example generation for all of them.

Semi-formal Verification

In addition to classical reachability analysis, TranSyT offers an automated two-phase simulation-verification hybrid scheme. Simulation follows a branching scheme that generates traces as divergent as possible (interleaved traces will be rejected). Traces are stored for further analysis. The second phase will select a number of simulation traces as seed of a guided-traversal algorithm. Guided-traversal exploits the behavioral information in the traces to efficiently identify additional states. On-the-fly invariant verification can be carried out during both phases.

Relative-time Verification

TranSyT offers invariant verification of timed systems based on the relative-timing paradigm. TSIF events can be annotated with mix-max delays. If it exists, the tool provides a timed counter-example for some invariant. Otherwise, TranSyT provides a set of graphic structures that inform the user about how the execution of events in the system is ordered due to timing. Note that not all existing orderings are provided, but just those that are relevant to prove the invariants under verification.

Tool Efficiency

Experiments show that the special characteristics of asynchronous concurrent systems motivate the necessity of developing specialized traversal algorithms for them. The comparative study between some of the most common existing traversal strategies and a number of strategies specially developed for asynchronous systems show a clear advantatge in favor of TranSyT. The tools selected for that comparison are NuSMV and VIS. Our results highlight the importance of properly selecting the verification tool according to the type of system being analyzed. TranSyT shows that, in general, verification time can be greatly reduced, and in some cases specialized techniques will dictate the difference between enabling an efficient verification or collapsing the capabilities of the selected computer (see our benchmark set).

People involved

Developers: Enric Pastor, Marco A. Peña and Marc Solé.

Contributors: Jordi Cortadella, Alex Smirnov and Alex Kondratyev

News