Specifying and verifying liveness properties of QLOCK in CafeOBJ


Norbert Preining
JAIST, Research Center for Software Verification, Japan


14th International Workshop on Termination
July 2014, Vienna, Austria.


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.

Leave a comment

Your email address will not be published. Required fields are marked *