The search functionality is under construction.

The search functionality is under construction.

Proofs written in algebraic specification languages are called proof scores. The proof score approach to design verification is attractive because it provides a flexible way to prove that designs for systems satisfy properties. Thus far, however, the approach has focused on safety properties. In this paper, we describe a way to verify that designs for systems satisfy liveness properties with the approach. A mutual exclusion protocol using a queue is used as an example. We describe the design verification and explain how it is verified that the protocol satisfies the lockout freedom property.

- Publication
- IEICE TRANSACTIONS on Information Vol.E91-D No.12 pp.2804-2817

- Publication Date
- 2008/12/01

- Publicized

- Online ISSN
- 1745-1361

- DOI
- 10.1093/ietisy/e91-d.12.2804

- Type of Manuscript
- PAPER

- Category
- Fundamentals of Software and Theory of Programs

The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.

Copy

Kazuhiro OGATA, Kokichi FUTATSUGI, "Proof Score Approach to Verification of Liveness Properties" in IEICE TRANSACTIONS on Information,
vol. E91-D, no. 12, pp. 2804-2817, December 2008, doi: 10.1093/ietisy/e91-d.12.2804.

Abstract: Proofs written in algebraic specification languages are called proof scores. The proof score approach to design verification is attractive because it provides a flexible way to prove that designs for systems satisfy properties. Thus far, however, the approach has focused on safety properties. In this paper, we describe a way to verify that designs for systems satisfy liveness properties with the approach. A mutual exclusion protocol using a queue is used as an example. We describe the design verification and explain how it is verified that the protocol satisfies the lockout freedom property.

URL: https://global.ieice.org/en_transactions/information/10.1093/ietisy/e91-d.12.2804/_p

Copy

@ARTICLE{e91-d_12_2804,

author={Kazuhiro OGATA, Kokichi FUTATSUGI, },

journal={IEICE TRANSACTIONS on Information},

title={Proof Score Approach to Verification of Liveness Properties},

year={2008},

volume={E91-D},

number={12},

pages={2804-2817},

abstract={Proofs written in algebraic specification languages are called proof scores. The proof score approach to design verification is attractive because it provides a flexible way to prove that designs for systems satisfy properties. Thus far, however, the approach has focused on safety properties. In this paper, we describe a way to verify that designs for systems satisfy liveness properties with the approach. A mutual exclusion protocol using a queue is used as an example. We describe the design verification and explain how it is verified that the protocol satisfies the lockout freedom property.},

keywords={},

doi={10.1093/ietisy/e91-d.12.2804},

ISSN={1745-1361},

month={December},}

Copy

TY - JOUR

TI - Proof Score Approach to Verification of Liveness Properties

T2 - IEICE TRANSACTIONS on Information

SP - 2804

EP - 2817

AU - Kazuhiro OGATA

AU - Kokichi FUTATSUGI

PY - 2008

DO - 10.1093/ietisy/e91-d.12.2804

JO - IEICE TRANSACTIONS on Information

SN - 1745-1361

VL - E91-D

IS - 12

JA - IEICE TRANSACTIONS on Information

Y1 - December 2008

AB - Proofs written in algebraic specification languages are called proof scores. The proof score approach to design verification is attractive because it provides a flexible way to prove that designs for systems satisfy properties. Thus far, however, the approach has focused on safety properties. In this paper, we describe a way to verify that designs for systems satisfy liveness properties with the approach. A mutual exclusion protocol using a queue is used as an example. We describe the design verification and explain how it is verified that the protocol satisfies the lockout freedom property.

ER -