The Second International Conference on Availability, Reliability and Security (ARES'07) (2007)
Apr. 10, 2007 to Apr. 13, 2007
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ARES.2007.89
Bastian Braun , University of Hamburg
Synthesizing fault-tolerant systems from fault-intolerant systems simplifies design of fault-tolerance. Arora and Kulkarni developed a method and a tool to synthesize fault-tolerance under the assumption that specifications are not history-dependent (fusion-closed). Later, Gartner and Jhumka removed this assumption by presenting a modular extension of the Arora-Kulkarni method. This paper presents an implementation of the Gartner-Jhumka method which is evaluated on several examples. As additional safety net, we have added automatic verification of the results using the model checker Spin. In the context of this work, a fault in the Gartner-Jhumka method has been found. Though this fault is rare and does not cause incorrect results, there might be no result at all
formal specification, program verification, software fault tolerance
B. Braun, "FCPre: Extending the Arora-Kulkarni Method of Automatic Addition of Fault-Tolerance," The Second International Conference on Availability, Reliability and Security (ARES'07)(ARES), Vienna, Austria, 2007, pp. 967-974.