Verification of Error Recovery Specification for Distributed Data by Using Colored Petri Nets

Masaharu AKATSU; Tomohiro MURATA; Kenzo KURIHARA

Verification of Error Recovery Specification for Distributed Data by Using Colored Petri Nets

Masaharu AKATSU, Tomohiro MURATA, Kenzo KURIHARA

Full Text Views

0

Cite this

Summary :

In systems where the same data are distributed in plural memories, data consistency must be maintained after a failure. It is important to verify that error recovery specifications guarantee the data consistency, and it is difficult because system status is nondeterministic after a failure occurs. In this paper, a method of modeling and verifying error recovery specifications by using colored Petri nets is proposed. First, the concept of data freshness is introduced to describe the relationship between the data explicitly. Then, a flow-chart that describes data renewal sequences is converted into a Petri net. Failure events and recovery procedures are added to the model. Consistency is verified by investigating reachable markings and by checking for the existence of states in which data freshness is contradictory. The number of reachable markings is generally enormous and sometimes infinite. Thus, the condition in which two markings are identified for verification is studied. The introduction of the equivalence relation itno reachable markings reduces the number of the markings to be verified. The usefulness of the proposed approach is demonstrated by a read/write process of a disk controller with a built-in cache memory. This example makes it clear that the analysis is helpful not only for checking whether the data is consistent, but also for designing the recovery procedures maintaining the data consistency.

Publication: IEICE TRANSACTIONS on Fundamentals Vol.E74-A No.10 pp.3159-3167

Publication Date: 1991/10/25

Publicized

Online ISSN

DOI

Type of Manuscript: Special Section PAPER (Special Issue on Petri Nets and Discrete Event Systems)

Category

Authors

Masaharu AKATSU
Tomohiro MURATA
Kenzo KURIHARA

Keyword

Cite this

Copy

Masaharu AKATSU, Tomohiro MURATA, Kenzo KURIHARA, "Verification of Error Recovery Specification for Distributed Data by Using Colored Petri Nets" in IEICE TRANSACTIONS on Fundamentals, vol. E74-A, no. 10, pp. 3159-3167, October 1991, doi: .
Abstract: In systems where the same data are distributed in plural memories, data consistency must be maintained after a failure. It is important to verify that error recovery specifications guarantee the data consistency, and it is difficult because system status is nondeterministic after a failure occurs. In this paper, a method of modeling and verifying error recovery specifications by using colored Petri nets is proposed. First, the concept of data freshness is introduced to describe the relationship between the data explicitly. Then, a flow-chart that describes data renewal sequences is converted into a Petri net. Failure events and recovery procedures are added to the model. Consistency is verified by investigating reachable markings and by checking for the existence of states in which data freshness is contradictory. The number of reachable markings is generally enormous and sometimes infinite. Thus, the condition in which two markings are identified for verification is studied. The introduction of the equivalence relation itno reachable markings reduces the number of the markings to be verified. The usefulness of the proposed approach is demonstrated by a read/write process of a disk controller with a built-in cache memory. This example makes it clear that the analysis is helpful not only for checking whether the data is consistent, but also for designing the recovery procedures maintaining the data consistency.
URL: https://global.ieice.org/en_transactions/fundamentals/10.1587/e74-a_10_3159/_p

Copy

@ARTICLE{e74-a_10_3159,
author={Masaharu AKATSU, Tomohiro MURATA, Kenzo KURIHARA, },
journal={IEICE TRANSACTIONS on Fundamentals},
title={Verification of Error Recovery Specification for Distributed Data by Using Colored Petri Nets},
year={1991},
volume={E74-A},
number={10},
pages={3159-3167},
abstract={In systems where the same data are distributed in plural memories, data consistency must be maintained after a failure. It is important to verify that error recovery specifications guarantee the data consistency, and it is difficult because system status is nondeterministic after a failure occurs. In this paper, a method of modeling and verifying error recovery specifications by using colored Petri nets is proposed. First, the concept of data freshness is introduced to describe the relationship between the data explicitly. Then, a flow-chart that describes data renewal sequences is converted into a Petri net. Failure events and recovery procedures are added to the model. Consistency is verified by investigating reachable markings and by checking for the existence of states in which data freshness is contradictory. The number of reachable markings is generally enormous and sometimes infinite. Thus, the condition in which two markings are identified for verification is studied. The introduction of the equivalence relation itno reachable markings reduces the number of the markings to be verified. The usefulness of the proposed approach is demonstrated by a read/write process of a disk controller with a built-in cache memory. This example makes it clear that the analysis is helpful not only for checking whether the data is consistent, but also for designing the recovery procedures maintaining the data consistency.},
keywords={},
doi={},
ISSN={},
month={October},}

Copy

TY - JOUR
TI - Verification of Error Recovery Specification for Distributed Data by Using Colored Petri Nets
T2 - IEICE TRANSACTIONS on Fundamentals
SP - 3159
EP - 3167
AU - Masaharu AKATSU
AU - Tomohiro MURATA
AU - Kenzo KURIHARA
PY - 1991
DO -
JO - IEICE TRANSACTIONS on Fundamentals
SN -
VL - E74-A
IS - 10
JA - IEICE TRANSACTIONS on Fundamentals
Y1 - October 1991
AB - In systems where the same data are distributed in plural memories, data consistency must be maintained after a failure. It is important to verify that error recovery specifications guarantee the data consistency, and it is difficult because system status is nondeterministic after a failure occurs. In this paper, a method of modeling and verifying error recovery specifications by using colored Petri nets is proposed. First, the concept of data freshness is introduced to describe the relationship between the data explicitly. Then, a flow-chart that describes data renewal sequences is converted into a Petri net. Failure events and recovery procedures are added to the model. Consistency is verified by investigating reachable markings and by checking for the existence of states in which data freshness is contradictory. The number of reachable markings is generally enormous and sometimes infinite. Thus, the condition in which two markings are identified for verification is studied. The introduction of the equivalence relation itno reachable markings reduces the number of the markings to be verified. The usefulness of the proposed approach is demonstrated by a read/write process of a disk controller with a built-in cache memory. This example makes it clear that the analysis is helpful not only for checking whether the data is consistent, but also for designing the recovery procedures maintaining the data consistency.
ER -