Sessions with an unbounded number of agents

Akshay, S. ; Helouet, Loic ; Mukund, Madhavan (2015) Sessions with an unbounded number of agents In: 2014 14th International Conference on Application of Concurrency to System Design (ACSD), 23-27 Jun 2014, Tunis La Marsa, Tunisia.

Full text not available from this repository.

Official URL:

Related URL:


In web-based systems, agents engage in structured interactions called sessions. Sessions are logical units of computation, like transactions. However, unlike transactions, sessions cannot be isolated from each other. Thus, one has to verify that interference between sessions does not have unexpected side effects. A challenge in building a tractable model of sessions is that there is no a priori bound on the number of concurrently active agents and sessions in the system. Realistic specifications require agents to compare entities across sessions, but this must be modeled without assigning an unbounded set of unique identities to agents and sessions. We propose a model called session systems that allows an arbitrary number of concurrently active agents and sessions. Agents have a limited ability to remember partners across sessions. Configurations are represented as graphs and the operational semantics is described through graph-rewriting. Under reasonable restrictions, session systems turn out to be well-structured systems. This provides an effective verification algorithm for coverability properties. We show how to use this result to verify more elaborate business rules such as avoidance of conflicts of interest and the Chinese Wall Property.

Item Type:Conference or Workshop Item (Paper)
Source:Copyright of this article belongs to Institute of Electrical and Electronics Engineers.
Keywords:Verification; Services; WSTS
ID Code:114121
Deposited On:25 May 2018 04:57
Last Modified:25 May 2018 04:57

Repository Staff Only: item control page