
For FullText PDF, please login, if you are a member of IEICE,
or go to Pay Per View on menu list, if you are a nonmember of IEICE.

Proof Score Approach to Verification of Liveness Properties
Kazuhiro OGATA Kokichi FUTATSUGI
Publication
IEICE TRANSACTIONS on Information and Systems
Vol.E91D
No.12
pp.28042817 Publication Date: 2008/12/01 Online ISSN: 17451361
DOI: 10.1093/ietisy/e91d.12.2804 Print ISSN: 09168532 Type of Manuscript: PAPER Category: Fundamentals of Software and Theory of Programs Keyword: CafeOBJ, equations, observational transition systems (OTSs), rewriting, specification,
Full Text: PDF(261.7KB)>>
Summary:
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.

