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.
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.