For Full-Text 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
IEICE TRANSACTIONS on Information and Systems
Publication Date: 2008/12/01
Online ISSN: 1745-1361
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)>>
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.