TAPAAL 2.0 is a platform-independent modelling, simula-
tion and verification tool for extended timed-arc Petri nets. The tool
supports component-based modelling and offers an automated verifica-
tion of the EF, AG, EG and AF fragments of TCTL via translations to
Uppaal timed automata and via its own dedicated verification engine.
After more than three years of active development with a main focus on
usability aspects and on the efficiency of the verification algorithms, we
present the new version of TAPAAL 2.0 that has by now reached its ma-
turity and offers the first publicly available tool supporting the analysis
and verification of timed-arc Petri nets.