Proof Score Approach to Verification of Liveness Properties

Kazuhiro OGATA  Kokichi FUTATSUGI  

IEICE TRANSACTIONS on Information and Systems   Vol.E91-D   No.12   pp.2804-2817
Publication Date: 2008/12/01
Online ISSN: 1745-1361
DOI: 10.1093/ietisy/e91-d.12.2804
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Fundamentals of Software and Theory of Programs
CafeOBJ,  equations,  observational transition systems (OTSs),  rewriting,  specification,  

Full Text: PDF(261.7KB)>>
Buy this Article

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.