Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

Refinement based validation of an algorithm for detecting distributed termination

Mamoun Filali5, Philippe Mauran5, Gérard Padiou5, Philippe Quéinnec5 and Xavier Thirioux5

(5)  Institut de Recherche en Informatique de Toulouse, 118 route de Narbonne, 31062 Toulouse cedex 4, France
Abstract
We present the development and the validation of an algorithm for detecting the termination of diffusing computations. To the best of our knowledge, this is the first one which is based on the maximal paths generated by a diffusing computation. After an informal presentation of the algorithm, we proceed to its rigorous development within the framework of the Unity formalism and the assistance of the PVS proof system. The correctness of the algorithm is established through a refinement of an abstract model.

Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.106 • Server: MPWEB25
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)