Verification of error recovery specification for distributed data by using colored Petri net

Masaharu Akatsu, Tomohiro Murata, Kenzo Kurihara

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish
Title of host publicationProceedings - IEEE International Symposium on Circuits and Systems
PublisherPubl by IEEE
Pages930-933
Number of pages4
Volume2
Publication statusPublished - 1991
Externally publishedYes
Event1991 IEEE International Symposium on Circuits and Systems Part 4 (of 5) - Singapore, Singapore
Duration: 1991 Jun 111991 Jun 14

Other

Other1991 IEEE International Symposium on Circuits and Systems Part 4 (of 5)
CitySingapore, Singapore
Period91/6/1191/6/14

Fingerprint

Cache memory
Petri nets
Specifications
Data storage equipment
Controllers

ASJC Scopus subject areas

  • Electrical and Electronic Engineering
  • Electronic, Optical and Magnetic Materials

Cite this

Akatsu, M., Murata, T., & Kurihara, K. (1991). Verification of error recovery specification for distributed data by using colored Petri net. In Proceedings - IEEE International Symposium on Circuits and Systems (Vol. 2, pp. 930-933). Publ by IEEE.

Verification of error recovery specification for distributed data by using colored Petri net. / Akatsu, Masaharu; Murata, Tomohiro; Kurihara, Kenzo.

Proceedings - IEEE International Symposium on Circuits and Systems. Vol. 2 Publ by IEEE, 1991. p. 930-933.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Akatsu, M, Murata, T & Kurihara, K 1991, Verification of error recovery specification for distributed data by using colored Petri net. in Proceedings - IEEE International Symposium on Circuits and Systems. vol. 2, Publ by IEEE, pp. 930-933, 1991 IEEE International Symposium on Circuits and Systems Part 4 (of 5), Singapore, Singapore, 91/6/11.
Akatsu M, Murata T, Kurihara K. Verification of error recovery specification for distributed data by using colored Petri net. In Proceedings - IEEE International Symposium on Circuits and Systems. Vol. 2. Publ by IEEE. 1991. p. 930-933
Akatsu, Masaharu ; Murata, Tomohiro ; Kurihara, Kenzo. / Verification of error recovery specification for distributed data by using colored Petri net. Proceedings - IEEE International Symposium on Circuits and Systems. Vol. 2 Publ by IEEE, 1991. pp. 930-933
@inproceedings{5da42fe7376749c78b85624113d3cf9e,
title = "Verification of error recovery specification for distributed data by using colored Petri net",
abstract = "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.",
author = "Masaharu Akatsu and Tomohiro Murata and Kenzo Kurihara",
year = "1991",
language = "English",
volume = "2",
pages = "930--933",
booktitle = "Proceedings - IEEE International Symposium on Circuits and Systems",
publisher = "Publ by IEEE",

}

TY - GEN

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

Y1 - 1991

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 contribution

VL - 2

SP - 930

EP - 933

BT - Proceedings - IEEE International Symposium on Circuits and Systems

PB - Publ by IEEE

ER -