TAPAAL Model Checker: Difference between revisions
Updated with the newest release and new engine for discrete time verification. |
|||
| Line 32: | Line 32: | ||
==External links== |
==External links== |
||
*[http://www.tapaal.net/ TAPAAL website, download] |
*[http://www.tapaal.net/ TAPAAL website, download] |
||
<ref>{{cite journal|coauthors=Alexandre David, Lasse Jacobsen, Morten Jacobsen, Kenneth Yrke Jørgensen, Mikael H. Møller, Jiří Srba|title=TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets|journal=TACAS|year=2012|volume=7214|series=LNCS|pages=492-497|doi=10.1007/978-3-642-28756-5_36|accessdate=17 January 2013}}</ref> |
|||
*[http://www.cs.aau.dk/en/research/des/ DES unit, Deptment of Computer Science, Aalborg University, Denmark] |
*[http://www.cs.aau.dk/en/research/des/ DES unit, Deptment of Computer Science, Aalborg University, Denmark] |
||
*[http://www.springerlink.com/content/6675215006510137/ TAPAAL: Editor, Simulator and Verifier of Timed-Arc Petri Nets by J. Byg, K.Y. Jørgensen and J. Srba, ATVA'09, Springer] |
*[http://www.springerlink.com/content/6675215006510137/ TAPAAL: Editor, Simulator and Verifier of Timed-Arc Petri Nets by J. Byg, K.Y. Jørgensen and J. Srba, ATVA'09, Springer] |
||
Revision as of 10:29, 17 January 2013
 | This article needs additional citations for verification. (February 2012) |
| Developer(s) | Aalborg University |
|---|---|
| Initial release | 2008 |
| Stable release | 2.2.1
/ December 5, 2012 |
| Preview release | 2.1.0
/ March 17, 2012 |
| Written in | C++ and GUI in Java |
| Operating system | Linux Mac OS X Microsoft Windows |
| Available in | English |
| Type | Model checking |
| License | Open Source |
| Website | http://www.tapaal.net |
TAPAAL is a tool for
- modelling, simulation and verification of
- Timed-Arc Petri nets
- developed at Department of Computer Science at AALborg University in Denmark
and it is available for Linux, Windows and Mac OS X platforms.
Timed-Arc Petri Net (TAPN) is a time extension of the classical Petri net model (a commonly used graphical model of distributed computations introduced by Carl Adam Petri in his disseration in 1962). The time extension considered in TAPN allows for explicit treatment of real-time, which is associated with the tokens in the net (each tokens has its own age) and arcs from places to transitions are labelled by time intervals that restrict the age of tokens that can be used in order to fire the respective transition. In TAPAAL tool a furter extension of this model with age invariants with transport arcs (which are more expressive than for example previously considered read-arcs) and with inhibitor arcs is implemented.
The TAPAAL tool offers a graphical editor for drawing TAPN models, simulator for experimenting with the designed nets and a verification environment that automatically answers logical queries formulated in a subset of CTL logic (essentially EF, EG, AF, AG formulae without nesting). It also allows the user to check whether a given net is k-bounded for a given number k. TAPAAL is equipped with its own verification engines distributed together with TAPAAL (one for continous time and one discrete time). Optionally, the user can automatically translate TAPAAL models into UPPAAL and rely on the UPPAAL verification engine.
External links
- DES unit, Deptment of Computer Science, Aalborg University, Denmark
- TAPAAL: Editor, Simulator and Verifier of Timed-Arc Petri Nets by J. Byg, K.Y. Jørgensen and J. Srba, ATVA'09, Springer
- An Efficient Translation of Timed-Arc Petri Nets to Networks of Timed Automata by J. Byg, K.Y. Jørgensen and J. Srba, ICFEM'09, Springer
- A Framework for Relating Timed Transition Systems and Preserving TCTL Model Checking by L. Jacobsen, M. Jacobsen, M.H. Møller and J. Srba, EPEW'10, Springer
- Verification of Timed-Arc Petri Nets by L. Jacobsen, M. Jacobsen, M.H. Møller and J. Srba, SOFSEM'11, Springer
 | This formal methods-related article is a stub. You can help Wikipedia by expanding it. |
- ^ "TAPAAL 2.0: Integrated Development Environment for Timed-Arc Petri Nets". TACAS. LNCS. 7214: 492–497. 2012. doi:10.1007/978-3-642-28756-5_36.
{{cite journal}}:|access-date=requires|url=(help); Unknown parameter|coauthors=ignored (|author=suggested) (help)