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.
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
- Open Source Conference 2015 Fukuoka, October 2015, Fukuoka, Japan.
CafeOBJ for real – Using an algebraic specification language as theorem prover. - MathLibre XXI Mathematical Software and Free Documents XXI, September 2015, Kyoto, Japan.
Algebraic specifications and Functional programming with CafeOBJ. - 43rd TRS Meeting Term Rewriting Meeting, September 2015, Morioka, Japan.
Quer durch den Gemüsegarten von CafeOBJ (Zick-zacking through the CafeOBJ’s vegetable garden). - CCA 2015: Twelfth International Conference on Computability and Complexity in Analysis, July 2015, Tokyo, Japan.
Norbert Preining. CafeOBJ for real – using an algebraic specification language as theorem prover for computational reals. - JAIST Verification Center Workshop, June 2015, Kaga, Ishikawa, Japan.
Norbert Preining. CafeOBJ in unusual surroundings. - 日本数式処理学会 第２４回大会 (24. Annual Meeting of the Japan Society for Symbolic and Algebraic Computation), June 2015, Tsukuba, Japan
Norbert Preining. CafeOBJ as symbolic and algebraic computation engine. - IMI Seminar, Kyushu University, March 2015, Hakata, Japan.
Introduction to CafeOBJ with case study - LOPSTR 2014: Logic-Based Program Synthesis and Transformation, September 2014, Canterbury, UK.
Norbert Preining, Kazuhiro Ogata and Kokichi Futatsugi. Liveness properties in CafeOBJ – a case study for meta-level specifications - WADT 2014: 22nd International Workshop on Algebraic Development Techniques, September 2014, Sinaia, Romania.
Norbert Preining, Kokichi Futatsugi, and Kazuhiro Ogata. Proving liveness properties using abstract state machines and n-visibility - WST 2014: 14th International Workshop on Termination, July 2014, Vienna Summer of Logic, Vienna, Austria.
Norbert Preining, Kazuhiro Ogata and Kokichi Futatsugi. Specifying and verifying liveness properties of QLOCK in CafeOBJ.
