Proof Score Approach to Verification of Liveness Properties
Kazuhiro Ogata, Kokichi Futatsugi · IEICE Transactions on Information and Systems · 2008
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.