TRANSYT: A Tool for the Verification of Asynchronous Concurrent Systems

摘要

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. A state of the art BDD package is integrated into the system, and a middleware extension provides support complex BDD manipulation strategies. TSIF (Transition System Interchange Format) is the main input language of TRANSYT. TSIF is a low-level language for describing asynchronous event-based systems, although synchronous systems can be also covered. Many formalisms can be mapped onto it: digital circuits, Petri nets, etc. TRANSYT integrates specialized algorithms for untimed reachability analysis based on disjunctive Transition Relation (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, and expands the horizon of timed verification to middle-size real examples.