loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
The Effect of the Specification Model on the Complexity of Adding Masking Fault Tolerance
October-December 2005 (vol. 2 no. 4)
pp. 348-355
ASCII Text
x 
 
Sandeep S. Kulkarni, Ali Ebnenasir, "The Effect of the Specification Model on the Complexity of Adding Masking Fault Tolerance," IEEE Transactions on Dependable and Secure Computing, vol. 2, no. 4, pp. 348-355, October-December, 2005.
 
 
BibTex
x
 
@article{ 10.1109/TDSC.2005.52,
author = {Sandeep S. Kulkarni and Ali Ebnenasir},
title = {The Effect of the Specification Model on the Complexity of Adding Masking Fault Tolerance},
journal ={IEEE Transactions on Dependable and Secure Computing},
volume = {2},
number = {4},
issn = {1545-5971},
year = {2005},
pages = {348-355},
doi = {http://doi.ieeecomputersociety.org/10.1109/TDSC.2005.52},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - JOUR
JO - IEEE Transactions on Dependable and Secure Computing
TI - The Effect of the Specification Model on the Complexity of Adding Masking Fault Tolerance
IS - 4
SN - 1545-5971
SP348
EP355
EPD - 348-355
A1 - Sandeep S. Kulkarni,
A1 - Ali Ebnenasir,
PY - 2005
KW - Index Terms- Fault-tolerance
KW - automatic addition of fault tolerance
KW - safety specification
KW - formal methods
KW - program synthesis.
VL - 2
JA - IEEE Transactions on Dependable and Secure Computing
ER -
 
In this paper, we investigate the effect of the representation of safety specification on the complexity of adding masking fault tolerance to programs—where, in the presence of faults, the program 1) recovers to states from where it satisfies its (safety and liveness) specification and 2) preserves its safety specification during recovery. Specifically, we concentrate on two approaches for modeling the safety specifications: 1) the bad transition (BT) model, where safety is modeled as a set of bad transitions that should not be executed by the program, and 2) the bad pair (BP) model, where safety is modeled as a set of finite sequences consisting of at most two successive transitions. If the safety specification is specified in the BT model, then it is known that the complexity of automatic addition of masking fault tolerance to high atomicity programs—where processes can read/write all program variables in an atomic step— is polynomial in the state space of the program. However, for the case where one uses the BP model to specify safety specification, we show that the problem of adding masking fault tolerance to high atomicity programs is NP-complete. Therefore, we argue that automated synthesis of fault-tolerant programs is likely to be more successful if one focuses on problems where safety can be represented in the BT model.

[1] S.S. Kulkarni and A. Arora, “Automating the Addition of Fault-Tolerance,” Proc. Sixth Int'l Symp. Formal Techniques in Real-Time and Fault-Tolerant Systems, pp. 82-93, 2000.
[2] F.C. Gärtner and A. Jhumka, “Automating the Addition of Failsafe Fault-Tolerance: Beyond Fusion-Closed Specifications,” Proc. Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT), pp. 183-198, Sept. 2004.
[3] B. Alpern and F.B. Schneider, “Defining Liveness,” Information Processing Letters, vol. 21, no. 4, pp. 181-185, Oct. 1985.
[4] A. Arora and M.G. Gouda, “Closure and Convergence: A Foundation of Fault-Tolerant Computing,” IEEE Trans. Software Eng., vol. 19, no. 11, pp. 1015-1027, Nov. 1993.
[5] S.S. Kulkarni, “Component-Based Design of Fault-Tolerance,” PhD thesis, Ohio State Univ., 1999.
[6] F.B. Schneider, “Enforcing Security Policies,” ACM Trans. Information and System Security, vol. 3, no. 1, pp. 30-50, 2000.
[7] E.W. Dijkstra, “Self-Stabilizing Systems in Spite of Distributed Control,” Comm. ACM, vol. 17, no. 11, 1974.
[8] A. Arora and S.S. Kulkarni, “Designing Masking Fault-Tolerance via Nonmasking Fault-Tolerance,” IEEE Trans. Software Eng., vol. 24, no. 6, pp. 435-450, June 1998.
[9] G. Varghese, “Self-Stabilization by Local Checking and Correction,” PhD thesis, Massachusetts Inst. Tech nology, 1993.
[10] S.S. Kulkarni and A. Ebnenasir, “A Framework for Automatic Synthesis of Fault-Tolerance,” Technical Report MSU-CSE-03-27, Michigan State Univ., http://www.cse.msu.edu/~sandeep/software/ Codesynthesis-framework/, 2003.
[11] M.R. Garey and D.S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness. Freeman, 1979.
[12] E.A. Emerson and E.M. Clarke, “Using Branching Time Temporal Logic to Synthesize Synchronization Skeletons,” Science of Computer Programming, vol. 2, no. 3, pp. 241-266, 1982.
[13] P. Attie and A. Emerson, “Synthesis of Concurrent Programs for an Atomic Read/Write Model of Computation,” ACM Trans. Programming Languages and Systems, vol. 23, no. 2, Mar. 2001.

Index Terms:
Index Terms- Fault-tolerance, automatic addition of fault tolerance, safety specification, formal methods, program synthesis.
Citation:
Sandeep S. Kulkarni, Ali Ebnenasir, "The Effect of the Specification Model on the Complexity of Adding Masking Fault Tolerance," IEEE Transactions on Dependable and Secure Computing, vol. 2, no. 4, pp. 348-355, Oct.-Dec. 2005, doi:10.1109/TDSC.2005.52
Usage of this product signifies your acceptance of the Terms of Use.