CafeOBJ

This page collects work I am doing in algebraic specification and verification. The language used is CafeOBJ, which is a a new generation algebraic specification and programming language. As a direct successor of OBJ, it inherits all its features (flexible mix-fix syntax, powerful typing system with sub-types, and sophisticated module composition system featuring various kinds of imports, parameterised modules, views for instantiating the parameters, module expressions, etc.) but it also implements new paradigms such as rewriting logic and hidden algebra, as well as their combination.

cafeobj-logo

QLock Fairness

QLOCK is a well known protocol of mutual exclusion, and many implementation and verifications in CafeOBJ are available. I have extended the current proofs of mutual exclusion to cover also fairness, i.e., any agent will eventually enter the queue and eventually go into critical section. Since this requires fairness of the execution, some meta constructs have to be reflected back into the specification. My approach is to include an execution sequence in the modeling. The current code including documentation is her: qlock-freefair.cafe, which in turn needs the specification of the QLOCK protocol as given by Prof. Futatsugi for the lecture on Algebraic Formal Methods. The two files can be downloaded from there: qlock-sysProp.cafe and qlock-invPS.cafe.

I am in the process of writing up a document providing the logical background and connections of this methodology.

CloudSync

I devised, specified and verified a simplified cloud synchronization protocol. Arbitrary many PCs can connect to a central cloud, fetch the value from the cloud, compare it with their own value, and update the cloud or their own value depending on which is larger. A detailed explanation can be found in a (part of) a presentation I gave during a work meeting: cloudsync.pdf.

The CafeOBJ specification and proof score are both available in cloudsync.cafe.

An independent implementation and verification of this protocol has been done in Constructor-based Inductive Theorem Prover (CITP) by Daniel Gaina.

Conference presentations and publications

Recent posts tagged CafeOBJ