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

XPeer (CCS):

* initialstate Controller agent Controller = login.(tau.'reject.Controller + tau.'begin.'accept.Controller) + logout.'end.Controller;

XPeer (CCS):

* initialstate Application agent Application = begin.App; agent App = upload.App + end.Application;

XPeer (CCS):

* initialstate Client agent Client = 'login.(accept.'upload.'upload.'logout.Client + reject.Client);

Add CCS peerAdd 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)