Programming-logic analysis of fault tolerance

expected performance of self-stabilisation

Carroll C. Morgan, Annabelle McIver

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contribution

Abstract

Formal proofs of functional correctness and rigorous analyses of fault tolerance have, traditionally, been separate processes. In the former a programming logic (proof) or computational model (model checking) is used to establish that all the system's behaviours satisfy some (specification) criteria. In the latter, techniques derived from engineering are used to determine quantitative properties such as probability of failure (given failure of some component) or expected performance (an average measure of execution time, for example).

To combine the formality and the rigour requires a quantitative approach within which functional correctness can be embedded. Programming logics for probability are capable in principle of doing so, and in this article we illustrate the use of the probabilistic guarded-command language (pGCL) and its logic for that purpose.

We take self-stabilisation as an example of fault tolerance, and present program-logical techniques for determining, on the one hand, that termination occurs with probability one and, on the other, the the expected time to termination is bounded above by some value. An interesting technical novelty required for this is the recognition of both "angelic" and "demonic" refinement, reflecting our simultaneous interest in both upper- and lower bounds.

Original languageEnglish
Title of host publicationRIGOROUS DEVELOPMENT OF COMPLEX FAULT-TOLERANT SYSTEMS
EditorsMichael Butler, Cliff Jones, Alexander Romanovsky, Elena Troubitsyna
Place of PublicationBerlin; New York
PublisherSpringer, Springer Nature
Pages288-305
Number of pages18
ISBN (Print)9783540482659
DOIs
Publication statusPublished - 2006
EventWorkshop on Rigorous Open Development Environment for Complex Systems - Newcastle upon Tyne
Duration: 1 Jan 2005 → …

Publication series

NameLecture Notes in Computer Science
PublisherSPRINGER-VERLAG BERLIN
Volume4157
ISSN (Print)0302-9743

Conference

ConferenceWorkshop on Rigorous Open Development Environment for Complex Systems
CityNewcastle upon Tyne
Period1/01/05 → …

Cite this