Sessions with an unbounded number of agents

Abstract : —In web-based business systems, agents engage in structured interactions, called sessions. Sessions are logical units of computations, like transactions. However, unlike transactions, sessions cannot be isolated from each other. Thus, one has to verify such systems in the presence of both intended and unintended interference between sessions. The main 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 has to be modelled without assigning an unbounded set of unique identities to active agents and sessions. We propose a model called session systems that allows for an arbitrary number of concurrently active agents and sessions. Agents are equipped with a limited ability to remember partners across sessions. Configurations are represented as graphs and the operational semantics is described through graph-rewriting. We show that, under reasonable restrictions, session systems are well-structured systems. This provides an effective verification algorithm for simple coverability properties. We then show how to use this result to verify more elaborate business rules such as avoidance of conflicts of interest and the Chinese Wall Property.
Type de document :
Communication dans un congrès
14th International Conference on Application of Concurrency to System Design, Jun 2014, Tunis, Tunisia. IEEE, 14th International Conference on Application of Concurrency to System Design, 14th International Conference on Application of Concurrency to System Design. 〈http://petrinets2014.cnam.fr/acsd.php〉
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01088994
Contributeur : Loic Helouet <>
Soumis le : samedi 29 novembre 2014 - 21:30:09
Dernière modification le : mercredi 16 mai 2018 - 11:24:06
Document(s) archivé(s) le : vendredi 14 avril 2017 - 23:28:14

Fichier

SessionsACSD.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01088994, version 1

Citation

S Akshay, Loïc Hélouët, Madhavan Mukund. Sessions with an unbounded number of agents. 14th International Conference on Application of Concurrency to System Design, Jun 2014, Tunis, Tunisia. IEEE, 14th International Conference on Application of Concurrency to System Design, 14th International Conference on Application of Concurrency to System Design. 〈http://petrinets2014.cnam.fr/acsd.php〉. 〈hal-01088994〉

Partager

Métriques

Consultations de la notice

449

Téléchargements de fichiers

109