The Community for Technology Leaders
The Second International Conference on Availability, Reliability and Security (ARES'07) (2007)
Vienna, Austria
Apr. 10, 2007 to Apr. 13, 2007
ISBN: 0-7695-2775-2
pp: 967-974
Bastian Braun , University of Hamburg
ABSTRACT
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
INDEX TERMS
formal specification, program verification, software fault tolerance
CITATION

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.
doi:10.1109/ARES.2007.89
81 ms
(Ver 3.3 (11022016))