TY - JOUR
T1 - Verification of error recovery specification for distributed data by using colored Petri net
AU - Akatsu, Masaharu
AU - Murata, Tomohiro
AU - Kurihara, Kenzo
PY - 1991/12/1
Y1 - 1991/12/1
N2 - In systems where the same data are distributed in plural memories, it is important for designers to verify that error recovery procedures maintain data consistency after a failure. A modeling and validation method of error recovery specifications by using colored Petri nets is proposed. The analysis of reachable states is useful to verify consistency. The introduction of the equivalence relation into reachable states reduces the number of the states to be verified. The proposed approach was applied to read/write control of a disk controller with a built-in cache memory.
AB - In systems where the same data are distributed in plural memories, it is important for designers to verify that error recovery procedures maintain data consistency after a failure. A modeling and validation method of error recovery specifications by using colored Petri nets is proposed. The analysis of reachable states is useful to verify consistency. The introduction of the equivalence relation into reachable states reduces the number of the states to be verified. The proposed approach was applied to read/write control of a disk controller with a built-in cache memory.
UR - http://www.scopus.com/inward/record.url?scp=0026290322&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=0026290322&partnerID=8YFLogxK
M3 - Conference article
AN - SCOPUS:0026290322
SN - 0271-4310
VL - 2
SP - 930
EP - 933
JO - Proceedings - IEEE International Symposium on Circuits and Systems
JF - Proceedings - IEEE International Symposium on Circuits and Systems
T2 - 1991 IEEE International Symposium on Circuits and Systems Part 4 (of 5)
Y2 - 11 June 1991 through 14 June 1991
ER -