Automated Verification of Asynchronous Communicating Systems
(with TLA+)
Model Checker
Help
Examples
Download
About
A Client-Server System.
The Server is split into a controller and an application.
The controller accepts or rejects the client, and begins/ends the application when needed.
Communication Model(s):
analyzed_by_pf,,login,accept,reject,upload,logout,begin,end message_cap,BOUND <- 3,login message_cap,BOUND <- 3,accept message_cap,BOUND <- 3,reject message_cap,BOUND <- 3,upload message_cap,BOUND <- 3,logout message_cap,BOUND <- 3,begin message_cap,BOUND <- 3,end
X
Peer (CCS):
* initialstate Client agent Client = 'login.(accept.'upload.'upload.'logout.Client + reject.Client);
X
Peer (CCS):
* initialstate Application agent Application = begin.App; agent App = upload.App + end.Application;
X
Peer (CCS):
* initialstate Controller agent Controller = login.(tau.'reject.Controller + tau.'begin.'accept.Controller) + logout.'end.Controller;
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)