http://www.jaist.ac.jp/~kokichi/lecture/1609NII/
Web Page for the Course of Lectures:
Introduction to Specification Verification with CafeOBJ
on 16(Fri,13:30-17:00) + 23(Fri,13:30-17:00) September 2016
at NII, Tokyo, Japan
Lecturer:
FUTATSUGI,Kokichi
(
JAIST)
(Send e-mail to
FUTATSUGI "futatsugi at jaist.ac.jp" for queries)
Overview
CafeOBJ is a most advanced algebraic formal specification language
system with rewriting/reduction engine which can be used for
interactive verification. Proof scores are scripts for verifications
and provide versatile ways to prove properties of specifications. The
lectures give foundations and techniques of CafeOBJ/ProofScores by
using elementary examples of natural numbers, lists, sequences, sets
and a simple mutual exclusion protocol.
A new topic of this year's course is "automation of case analyses with
Specification Calculus" that helps to achieve non-trivial
interactive verifications systematically.
Goal of the Course
To obtain the following abilities
by solving several simple but non-trivial examples
with CafeOBJ Language System.
(1) formalizing domain, requirement, design specifications
based on the formal systems like sets, functions/maps, algebras.
(2) analysing and/or verifying the obtained formal specifications.
Preliminary Materials:
Lecture Schedule and Materials
- [Sep.16 (Fri) 13:30-15:00]
Basics of CafeOBJ and Peano Style Natural Numbers
- [Sep.16 (Fri) 15:15-16:45]
List, Seq, Set and Specification Calculus
- [Sep.16 (Fri) 16:45-17:00]
Questions and Answers
- [Sep.23 (Fri) 13:30-15:00]
Modeling, Specification, and Simulation of
Mutual Exclusion Protocol QLOCK
- [Sep.23 (Fri) 15:15-16:45]
Proof Score Development for QLOCK with Specification Calculus
- [Sep.23 (Fri) 16:45-17:00]
Questions and Answers
Installation of CafeOBJ Language System
Each attendee is expected to install CafeOBJ System version
1.5.5 (or later) to his/her own personal computer for executing examples,
exercises, and assignments of the lectures. The specs and proof scores
of the lectures are prepared for the version 1.5.5
You can obtain CafeOBJ binaries for
Linux, MacOS, and Windows from the following web page.
CafeOBJ Web Page
http://www.jaist.ac.jp/~kokichi/lecture/1609NII/