Specifying and verifying liveness properties of QLOCK in CafeOBJ

ABSTRACT. We provide an innovative development of algebraic specifications and proof scores in CafeOBJ of QLOCK's safety and liveness properties. The particular interest of the development is two-fold: Firstly, it extends base specifications in order-sorted and rewriting logics to a meta-level, which requires behavioral logic, thus using the three logics together to achieve the proofs. Secondly, we use a search predicate and covering state patterns that allow us to prove the validity of a property over all possible one step transitions, by which safety and liveness properties in the base and meta level can be proven.