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.
|ジャーナル||Proceedings - IEEE International Symposium on Circuits and Systems|
|出版ステータス||Published - 1991 12 1|
|イベント||1991 IEEE International Symposium on Circuits and Systems Part 4 (of 5) - Singapore, Singapore|
継続期間: 1991 6 11 → 1991 6 14
ASJC Scopus subject areas