Geodesic
Formal Verification of Signature-monitoring Mechanisms by Model Checking
Computer Science and Information Systems, Tome 9 (2012) no. 4.

Voir la notice de l'article provenant de la source Computer Science and Information Systems website

In recent decades, reliability in the presence of transient faults has been a significant problem. To mitigate the effects of transient faults, fault-tolerant techniques are proposed. However, validating the effectiveness of fault-tolerant techniques is another problem. In this paper, we present an original approach to evaluate the effectiveness of signature-monitoring mechanisms. The approach is based on model-checking principles. First, the fault tolerant model is proposed using step-operational semantics. Second, the fault model is refined into a state transition system that is translated into the input program of the symbolic model checker NuSMV. Using NuSMV, two reprehensive signature-monitoring algorithms are verified. The approach avoids the state space explosion problem and the verification was completed with practical time. The verification results reveal some undetected errors, which have not been previously observed.
Keywords: software fault-tolerance, model checking, formal verification, fault tolerance, signature monitoring mechanisms 
@article{CSIS_2012_9_4_a4,
     author = {Lanfang Tan and Qingping Tan and Jianjun Xu and Huiping Zhou},
     title = {Formal {Verification} of {Signature-monitoring} {Mechanisms} by {Model} {Checking}},
     journal = {Computer Science and Information Systems},
     publisher = {mathdoc},
     volume = {9},
     number = {4},
     year = {2012},
     url = {http://geodesic.mathdoc.fr/item/CSIS_2012_9_4_a4/}
}
TY  - JOUR
AU  - Lanfang Tan
AU  - Qingping Tan
AU  - Jianjun Xu
AU  - Huiping Zhou
TI  - Formal Verification of Signature-monitoring Mechanisms by Model Checking
JO  - Computer Science and Information Systems
PY  - 2012
VL  - 9
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/CSIS_2012_9_4_a4/
ID  - CSIS_2012_9_4_a4
ER  - 
%0 Journal Article
%A Lanfang Tan
%A Qingping Tan
%A Jianjun Xu
%A Huiping Zhou
%T Formal Verification of Signature-monitoring Mechanisms by Model Checking
%J Computer Science and Information Systems
%D 2012
%V 9
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/CSIS_2012_9_4_a4/
%F CSIS_2012_9_4_a4
Lanfang Tan; Qingping Tan; Jianjun Xu; Huiping Zhou. Formal Verification of Signature-monitoring Mechanisms by Model Checking. Computer Science and Information Systems, Tome 9 (2012) no. 4. http://geodesic.mathdoc.fr/item/CSIS_2012_9_4_a4/