Preliminary Formal Analysis of TTA Startup

John Rushby

CSL Technical Report, February 2003

This report describes preliminary experiments that led to the much more comprehensive analysis described in this paper

Abstract

We formally specify the TTA startup algorithm of Paulitsch and Steiner in the SAL language. Using the SALenv model checker, we confirm that the algorithm succeeds in starting the cluster after at most one collision. We explore alternative algorithms and system parameters, and investigate behavior in the presence of faults. The limitations of finite-state modeling are discussed, together with plans for more comprehensive analysis and verification.

Paper

PDF

BibTeX Entry

           TBD

Having trouble reading our papers?
Return to John Rushby's bibliography page
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page