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