Proof Score Approach to Verification of Liveness Properties

概要

論文の詳細を見る
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.
電子情報通信学会の論文
2008-12-01