Back to Search
Start Over
Scalable Correct-by-Construction Conversation Protocols with Event-B: Validation, Experiments and Benchmarks
- Source :
- ICECCS
- Publication Year :
- 2018
- Publisher :
- IEEE, 2018.
-
Abstract
- In this paper, we address the design of distributed systems composed of peers (state-transitions systems) communicating through message exchanges. We consider choreographies as the ground formal model allowing a developer to describe and specify peers coordination as a set of conversations, i.e., all sequences of messages exchanged between the communicating peers. Proceeding this way does not require building the individual peers, nor their composition; they may be obtained by choreography projection. The correctness of the preservation of such messages exchanges by each peer obtained after projection is a key issue, known as the realizability problem. In our previous work [1], we have proposed a set of composition operators allowing designers to build realizable choreographies that are represented by conversation protocols (CPs). We rely on the correct-by-construction Event-B method to prove that each CP constructed using our operators is realizable. In this paper, we show how our approach applies and scales to a set of use cases borrowed from the literature and used by the research community. We also show that our approach allows to detect failures and failure recovery in case realizability does not hold
- Subjects :
- Theoretical computer science
Correctness
Computer science
media_common.quotation_subject
020207 software engineering
02 engineering and technology
Choreography
Set (abstract data type)
020204 information systems
Realizability
0202 electrical engineering, electronic engineering, information engineering
Key (cryptography)
Use case
Conversation
Projection (set theory)
media_common
Subjects
Details
- Database :
- OpenAIRE
- Journal :
- 2018 23rd International Conference on Engineering of Complex Computer Systems (ICECCS)
- Accession number :
- edsair.doi...........bb0ede7533344abdfd2df115cccc159a
- Full Text :
- https://doi.org/10.1109/iceccs2018.2018.00034