Formal verification of dependable distributed protocols |
| |
| Affiliation: | 1. Korea Institute of Civil Engineering and Building Technology, 10223 Goyang-daero, Ilsanseo-gu, Goyang-si, Gyeonggi-do 10223, Republic of Korea;2. Department of Architectural Engineering, University of Seoul, 163 Seoulsirip-daero, Dongdaemun-gu, Seoul-si 02504, Republic of Korea;1. Institut de Chimie et Procédés pour l''Energie, l''Environnement et la Santé (ICPEES), CNRS/University of Strasbourg, 25 rue Becquerel, Strasbourg, France;2. Photoactivated Processes Unit, IMDEA Energy Institute, Móstoles, 28935, Madrid, Spain;3. Institut de Physique et de Chimie des Matériaux de Strasbourg (IPCMS), CNRS/University de Strasbourg, 23 rue du Loess, Strasbourg, France;1. Department of Earth Sciences, Indian Institute of Technology Kanpur, Kanpur 208016, India;2. Department of Civil Engineering, Indian Institute of Technology Kanpur, Kanpur, 208016, India;3. Superintendent Archaeologist, Archaeological Survey of India (ASI), Bhopal Circle, Bhopal, Madhya Pradesh, India;4. Department of Ancient History, University of Allahabad, Allahabad, India;1. Department of Civil, Environmental and Architectural Engineering, University of Colorado, Boulder, CO 80309, USA;2. Department of Civil & Environmental Engineering, King Fahd University of Petroleum & Minerals, Dhahran 31261, Saudi Arabia;3. Interdisciplinary Research Center for Construction and Building Materials, King Fahd University of Petroleum & Minerals, Dhahran 31261, Saudi Arabia |
| |
| Abstract: | Dependable distributed systems often employ a hierarchy of protocols to provide timely and reliable services. Such protocols have both dependability and real-time attributes, and the verification of such composite services is a problem of growing complexity even when using formal approaches. Our intention in this paper is to exploit the modular design aspects appearing in most dependable distributed protocols to provide formal level of assurance for their correctness. We highlight the capability of our approach through a case study in formal modular specification and tool-assisted verification of a timestamp-based checkpointing protocol. Furthermore, during the process of verification, insights gained in such a stack of protocols have assisted in validating some additional properties those dealing with failure recovery. |
| |
| Keywords: | |
| 本文献已被 ScienceDirect 等数据库收录！ |
|
