Formal Verification of Signature-monitoring Mechanisms by Model Checking

Lanfang Tan1, Qingping Tan1, Jianjun Xu1 and Huiping Zhou1

  1. School Computer, National University of Defense Technology
    410073 Changsha, China
    {tanlanfang1022, eric.tan.6508, jjun.xu, icent}


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.

Key words

software fault-tolerance, model checking, formal verification, fault tolerance, signature monitoring mechanisms

Digital Object Identifier (DOI)

Publication information

Volume 9, Issue 4 (December 2012)
Special Issue on Recent Advances in Systems and Informatics
Year of Publication: 2012
ISSN: 1820-0214 (Print) 2406-1018 (Online)
Publisher: ComSIS Consortium

Full text

DownloadAvailable in PDF
Portable Document Format

How to cite

Tan, L., Tan, Q., Xu, J., Zhou, H.: Formal Verification of Signature-monitoring Mechanisms by Model Checking. Computer Science and Information Systems, Vol. 9, No. 4, 1431-1452. (2012)