Please use this identifier to cite or link to this item:
https://hdl.handle.net/2440/109019
Type: | Conference paper |
Title: | Formally proving and enhancing a self-stabilising distributed algorithm |
Author: | Coti, C. Lakos, C. Petrucci, L. |
Citation: | CEUR Workshop Proceedings, 2016 / Cabac, L., Kristensen, L., Rölke, H. (ed./s), vol.1591, pp.255-274 |
Publisher: | CEUR |
Issue Date: | 2016 |
ISSN: | 1613-0073 |
Conference Name: | International Workshop on Petri Nets and Software Engineering (PNSE '16) (20 Jun 2016 - 21 Jun 2016 : Torun, Poland) |
Editor: | Cabac, L. Kristensen, L. Rölke, H. |
Statement of Responsibility: | Camille Coti, Charles Lakos, and Laure Petrucci |
Abstract: | This paper presents the benefits of formal modelling and verification techniques for self-stabilising distributed algorithms. An algorithm is studied, that takes a set of processes connected by a tree topology and converts it to a ring configuration. The Coloured Petri net model not only facilitates the proof that the algorithm is correct and self-stabilising but also easily shows that it enjoys new properties of termination and silentness. Further, the formal results show how the algorithm can be simplified without loss of generality. |
Description: | Includes the International Workshop on Biological Processes & Petri Nets 2016 |
Rights: | Copyright © 2016 for the individual papers by the papers' authors. Copying permitted for private and academic purposes. This volume is published and copyrighted by its editors. |
Published version: | http://ceur-ws.org/Vol-1591/ |
Appears in Collections: | Aurora harvest 8 Computer Science publications |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
RA_hdl_109019.pdf Restricted Access | Restricted Access | 725.17 kB | Adobe PDF | View/Open |
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.