Click on the pictures to see large version.


The main editor window of TAPAAL.


The improved query designer makes it super easy to create queries without a detailed knowledge of the concrete syntax. Queries can be by expert users edited also manually.

TAPAAL provides a standalone verification engines as well as verification via a translation to UPPAAL timed automata. The integrating within the TAPAAL GUI is seemless the answers are displayed directly in TAPAAL.


Simulation of a net behaviour can be done step by step, and error traces are loaded into the simulator allowing for an easy visualization of counter-examples.

Workflow Analysis

The workflow analysis module allows to verify normal and strong soundness of timed-arc workflow nets, including a detailed debugging information in case the net is not sound.