Prior to Download
TAPAAL provides a standalone editor, simulator and verifier (called verifytapn) of timed-arc Petri nets. Optionally, for running an automated translation to timed automata, the user should install the latest development version of UPPAAL. Download UPPAAL from www.uppaal.org in the download section, and follow the instalation instructions from www.uppaal.org. You will need to locate the file verifyta that comes with the UPPAAL distribution and point TAPAAL to its location in the engine selection dialog from the Tools menu.
Before running TAPAAL make sure that JRE 6.0 or higher is installed on your system. Additionally, for Mac users we support only Mac OS X 10.9 and higher; on Mac OS X remember to allow applications downloaded from anywhere (in System Preferences and Security & Privacy tab or right-click on the application and choose “open”).
Binarier for Windows/Linux/Mac OS X:
- TAPAAL 3.6.1 for Windows Download (64 bit)
- TAPAAL 3.6.1 for Linux Download (64 bit)
- TAPAAL 3.6.1 for Mac Download (64 bit)
- Download TAPAAL GUI from Launchpad Source
- Download Continuous-Time TAPAAL Engine from Launchpad Source
- Download Discrete-Time TAPAAL Engine from Lauchpad Source
- Download Untimed P/T TAPAAL Engine from Launchpad Source
Please report any bugs that you might discover to our bug tracker.
See the tapaal changelog.
To install TAPAAL unpack the files for your platform and follow instructions in README.txt.
TAPAAL is licensed under tree licenses:
- The GUI tool is licensed under the Open Source Licence 3.0
- The reduction lib, used for automatic translation of TAPN models into UPPAAL Timed Automata and the discrete verification engine verifydtapn are licensed under the BSD License.
- The continuous-time verification engine verifytapn is licensed under GPL v2 license: http://www.gnu.org/licenses/gpl-2.0.txt
- beta release of TACPN GUI and unfolding engine (Win64, Linux64) and update synthesis experiments (zip)
- partial-order-experiments.zip - models with timed partial order reduction (blood transfusion, BAwPC, alternating bit protocol, fire alarm, Fischer, Lynch Shavit, MPEG-2, patient monitoring).
- Approximation of Time Intervals - Beta Release 3.0.99 (Win, Linux, Linux64, Mac, Mac64, case studies)
- Timed workflow nets - Beta Release 2.4.99 (Win, Linux, Linux64, Mac, Mac64, workflow case studies)
- NFM’14 case studies
- FHIES’12 Blood Transfusion Case Study and MEMICS’12 experiments
- Patient Monitoring System (PMS) and BAwPC Protocol (TAPAAL nets)
- Experiments in TAPAAL and UPPAAL (Alternating bit protocol, engine workshop, Fischer’s protocol, Lynch-Shavit protocol, medical workflow, MPEG2 encoder)
- Lynch-Shavit Protocol and MPEG-2 Encoding Algorithm (TAPAAL and UPPAAL models)
- UPPAAL version of Alternating Bit Protocold with query (not to be opened in TAPAAL)