![[Mail]](../../../../Images/umschlag.gif)
| Thomas Noll | Disclaimer | Last modified: 2005-03-04 08:02 UTC |
![[I2 logo]](../../../../Images/i2.gif)
![[RWTH logo]](../../../../Images/rwth-rot90.gif)
(Informatik 2)
HomeNewsJobsContactStaffTeachingResearchMOVES SeminarDFG-GK AlgoSynCS ChairsLuFG I2
Tools for the Specification and Verification of Concurrent Systems
Overview
| Tool | Developer | Implementation language | System description language | Semantic model | Logic | Model checking algorithm |
|---|---|---|---|---|---|---|
| Circal | University of South Australia | ? | XCircal | Finite-state transition systems | ? | (1) Explicit (2) OBDD-based |
| Concurrency Factory | SUNY at Stony Brook, NC State University | C++ | VPL (compiled into Facile) | Finite-state transition systems | Linear-time alternation-free modal mu-calculus | Explicit |
| Edinburgh Concurrency Workbench | University of Edinburgh | Standard ML | CCS | Finite-state transition systems | Modal mu-calculus | Explicit |
| FC2Tools | INRIA, Ecole des Mines | ? | Process algebra | Finite-state transition systems | ? | ? |
| FDR2 | Formal Systems Design and Development Inc. | ? | CSP | Finite-state transition systems | ? | Symbolic, on-the-fly |
| HyTech | University of Berkeley | C++ | Linear hybrid automata | ? | ICTL | Symbolic, region-based |
| JACK Tool Set | University of Pisa | Several | Transition systems | ? | ACTL | ? |
| Kronos | VERIMAG | ? | Timed automata | ? | TCTL | Symbolic, constraint-based |
| Mobility Workbench | Universities of Edinburgh and Uppsala | Standard ML | Pi-calculus | Transition systems | (only equivalence checking) | Explicit, on-the-fly |
| Model-Checking Kit | Technical University of Munich | Several | Communicating automata, Petri nets | Transition systems | LTL, CTL | Symbolic |
| North Carolina Concurrency Workbench | North Carolina State University | Standard ML | Several process algebras (Process Algebra Compiler) | Finite-state transition systems | Modal mu-calculus | Explicit |
| PEP | University of Hildesheim | C++ | Various (programs, automata, process algebras, nets) | Petri nets | CTL, LTL | by Esparza |
| SGM | Academia Sinica, Taiwan | ? | State graphs | Transition systems | ? | ? |
| SMV | Carnegie-Mellon University | ? | Automaton | Finite-state transition systems | CTL | Symbolic, OBDD-based |
| SPIN | Bell Laboratories | ANSI C | PROMELA | Finite-state transition systems | LTL | Explicit |
| Truth | Aachen University of Technology | Haskell/Java | CCS | Finite-state transition systems | Modal mu-calculus | Explicit, tableau-based |
| UPPAAL | Uppsala and Aalborg University | C++ | Timed automata | ? | Safety/liveness properties | ? |
Further Collections
- An overview of tools for working with Message Sequence Charts (MSCs)
- Electronic Tool Integration Platform
- Formal Methods (University of Oxford)
- Concurrency Tools (University of Oxford)
- Tools for Analyzing Reactive Systems (University of Berkeley)
- Computer-Aided Verification Tools Presented at CAV (University of Berkeley)
- BRICS Tools Home Page
- FME Formal Methods Tools Database (University of Newcastle)
- Mechanized Reasoning Systems (Stanford University)
- Verification Tools (Dortmund University)
- E.M. Clarke and J.M. Wing. Formal methods: State of the art and future directions. Technical Report CMU-CS-96-178, 1996. (PostScript.Gzip)
