{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,6]],"date-time":"2024-07-06T15:15:32Z","timestamp":1720278932969},"reference-count":0,"publisher":"National Library of Serbia","issue":"4","license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["ComSIS","COMPUT SCI INF SYST","COMPUT SCI INFORM SY","COMPUTER SCI INFORM","COMSIS J"],"published-print":{"date-parts":[[2012]]},"abstract":"<jats:p>In recent decades, reliability in the presence of transient faults has been a\n   significant problem. To mitigate the effects of transient faults,\n   fault-tolerant techniques are proposed. However, validating the effectiveness\n   of fault-tolerant techniques is another problem. In this paper, we present an\n   original approach to evaluate the effectiveness of signature-monitoring\n   mechanisms. The approach is based on model-checking principles. First, the\n   fault tolerant model is proposed using step-operational semantics. Second,\n   the fault model is refined into a state transition system that is translated\n   into the input program of the symbolic model checker NuSMV. Using NuSMV, two\n   reprehensive signature-monitoring algorithms are verified. The approach\n   avoids the state space explosion problem and the verification was completed\n   with practical time. The verification results reveal some undetected errors,\n   which have not been previously observed.<\/jats:p>","DOI":"10.2298\/csis120218056t","type":"journal-article","created":{"date-parts":[[2012,12,28]],"date-time":"2012-12-28T10:31:33Z","timestamp":1356690693000},"page":"1431-1451","source":"Crossref","is-referenced-by-count":2,"title":["Formal verification of signature-monitoring mechanisms by model checking"],"prefix":"10.2298","volume":"9","author":[{"given":"Lanfang","family":"Tan","sequence":"first","affiliation":[{"name":"School Computer, National University of Defense Technology, Changsha, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qingping","family":"Tan","sequence":"additional","affiliation":[{"name":"School Computer, National University of Defense Technology, Changsha, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jianjun","family":"Xu","sequence":"additional","affiliation":[{"name":"School Computer, National University of Defense Technology, Changsha, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huiping","family":"Zhou","sequence":"additional","affiliation":[{"name":"School Computer, National University of Defense Technology, Changsha, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"1078","container-title":["Computer Science and Information Systems"],"original-title":[],"language":"en","deposited":{"date-parts":[[2023,5,29]],"date-time":"2023-05-29T08:30:49Z","timestamp":1685349049000},"score":1,"resource":{"primary":{"URL":"https:\/\/doiserbia.nb.rs\/Article.aspx?ID=1820-02141200056T"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"references-count":0,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2012]]}},"URL":"https:\/\/doi.org\/10.2298\/csis120218056t","relation":{},"ISSN":["1820-0214","2406-1018"],"issn-type":[{"value":"1820-0214","type":"print"},{"value":"2406-1018","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}