Chevrou, Florent and Hurault, Aurélie and Mauran, Philippe and Quéinnec, Philippe Mechanized Refinement of Communication Models with TLA+. (2016) In: 5th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z (ABZ 2016), 23 May 2016 - 27 May 2016 (Linz, Austria).
|
(Document in English)
PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader 292kB |
Official URL: http://dx.doi.org/10.1007/978-3-319-33600-8_27
Abstract
In distributed systems, asynchronous communication is often viewed as a whole whereas there are actually many different interaction protocols whose properties are involved in the compatibility of peer compositions. A hierarchy of asynchronous communication models, based on refinements, is established and proven with the TLA+ Proof System. The work serves as a first step in the study of the substituability of the communication models when it comes to compatibility checking.
| Item Type: | Conference or Workshop Item (Paper) |
|---|---|
| Additional Information: | Thanks to Springer editor. This papers appears in Volume 9675 of Lecture Notes in Computer Science ISSN : 0302-9743 ISBN: 978-3-319-33599-5 The original PDF is available at: https://link.springer.com/chapter/10.1007/978-3-319-33600-8_27 |
| HAL Id: | hal-01535944 |
| Audience (conference): | International conference proceedings |
| Uncontrolled Keywords: | |
| Institution: | Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE) French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE) Université de Toulouse > Université Toulouse III - Paul Sabatier - UT3 (FRANCE) Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE) Université de Toulouse > Université Toulouse 1 Capitole - UT1 (FRANCE) |
| Laboratory name: | |
| Statistics: | download |
| Deposited On: | 31 May 2017 08:50 |
Repository Staff Only: item control page
