Session types for communicating systems in event-B

Abstract : Emergent systems are inherently communication-centered. Hence, a modeling strategy for those systems must provide the right abstractions for: (1) giving a general view of the communication patterns; (2) abstracting away from the interleaving and synchronization details; and (3) proving correct the communication schema. We propose a modeling strategy that integrates multiparty sessions types (MST) and Event-B (refinement calculus). We show how a global type, specifying the choreography that the agents must follow, can be translated into an Event-B machine describing the abstract behavior of the system (1 above). A refinement of the system leads to a model of the local types, describing declaratively the behavior of the agents involved (2 above). Relying on the type discipline and Rodin's (Event-B) theorem provers, we can prove the system correct (3 above). Our method does not require to reason about the system traces, thus easing the modeling task. We have also developed a tool that automatizes the process of generating the Event-B model from the MST specification. We illustrate our framework with three compelling distributed protocols.
Type de document :
Communication dans un congrès
Sascha Ossowski. SAC 2016, Proceedings of the 31st Annual Symposium on Applied Computing., Apr 2016, Pisa, Italy. ACM, 1, pp.1686-1693, 2016, Proceedings of the 31st Annual Symposium on Applied Computing. 〈10.1145/2851613.2851836〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01349564
Contributeur : Camilo Rueda <>
Soumis le : mercredi 27 juillet 2016 - 22:46:44
Dernière modification le : jeudi 17 novembre 2016 - 20:05:36

Identifiants

Citation

Carlos Olarte, Camilo Rueda. Session types for communicating systems in event-B. Sascha Ossowski. SAC 2016, Proceedings of the 31st Annual Symposium on Applied Computing., Apr 2016, Pisa, Italy. ACM, 1, pp.1686-1693, 2016, Proceedings of the 31st Annual Symposium on Applied Computing. 〈10.1145/2851613.2851836〉. 〈hal-01349564〉

Partager

Métriques

Consultations de la notice

40