Screenshots

Click on the pictures to see large version.

Editor

The main editor window of TAPAAL.

Verification

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

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.