Automated Verification of Asynchronous Communicating Systems
(with TLA+)
Model Checker
Help
Examples
Download
About
Notes
Please refer to the
help page
to learn how to use this website.
Numerous examples are also available
here
.
Communication Model(s):
Add CCS peer
Add LTS peer
Properties:
All peers terminate.
The network ends up empty.
No peer goes into a forbidden state.
No (global) deadlocks
Test properties
Infer all constraint sets (pessimistic)
Infer one constraint set (pessimistic)
Infer some constraint sets (optimistic)
Infer one constraint set (optimistic)
Infer all constraint sets (pessimistic, listened)
Infer one constraint set (pessimistic, listened)
Infer some constraint sets (optimistic, listened)
Infer one constraint set (optimistic, listened)
Known issues
Not user-friendly.
Using CCS peers with the current pretty printer makes it difficult to identify the peers (as their order may change).
CCS peers are not supported.
Constraint inference easily times out, because the analyzers don't flush their output buffers often enough (at all?).