Norbert Preining氏による【Specification and Verification of Software with CafeOBJ -Part 1】を公開

アクセリア株式会社の研究開発部社員であるNorbert Preining氏による、コラム連載を開始しました。

アクセリア株式会社 2018年02月27日

第12回:Specification and Verification of Software with CafeOBJ - Part 1 - Introducing CafeOBJ

「Overview on the blog series」
Software bugs are everywhere - the feared Blue Screen of Death, the mobile phone rebooting at the most inconvenient moment, games crashing. Most of these bugs are not serious problems, but there are other cases that are far more serious:
 ・Therac-25 X-ray machine which killed at least 5 patients by over-exposure
 ・Ariane 5 rocket, Flight 501 due to an overflow error
 ・Mars Climate Orbiter which crashed due to SI versus Imperial system inconsistency
 ・Intel Pentium F00F bug chip design error
 ・Toyota's Electronic Throttle Control System (ETCS)
 ・Heartbleed vulnerability of OpenSSL

While bugs will always remain, the question is how to deal with these kinds of bug. There is unsurmountable amount of literature on this topic, but it general falls into one of the following categories:
 ・program testing: subject the program to be checked to a large set of tests trying to exhaust all
  possible code paths
 ・post coding formal verification - model checking: given program code, model the behavior of the
  program in temporal logic and prove necessary properties
 ・pre coding specification and verification: start with a formal specification what the program should do,
   and verify that the specification is correct, that is, that it satisfies desirable properties

The first two items above are extremely successful and well developed. In this blog series we want to discuss the third item, specification and their verification.

This blog will introduce some general concepts about software and specifications, as well as introduce CafeOBJ as an algebraic specification language that is executable and thus can be used to verify the specification at the same time.

Further blog entries will introduce the CafeOBJ language in bit more detail, go through a simple example of cloud synchronization specification, and discuss more involved techniques and automated theorem proving using CafeOBJ.

「Why should we verify specifications?」
The value of formal specifications of software has been recognized since the early 80ies, and formal systems have been in development since then (Z, Larch and OBJ all originate at that time). On the other hand, actual use of these techniques did remain mostly in the academic surrounding - engineers and developers where mostly reluctant to learn highly mathematical languages to write specifications instead of writing code.

With the growth of interactivity, explosion of number of communication protocols (from low level TCP to high level SSL) with handshakes and data exchange sequences, the need for formal verification of these protocols, especially if they guard crucial data, has been increasing steadily.

「The CafeOBJ approach」
CafeOBJ is a member of the OBJ family and thus uses algebraic methods to describe specifications. This is in contrast to the Z system which uses set theory and lambda calculus.

Our aims in developing the language (as well as the system) CafeOBJ can be summarized as follows:
 ・provide a reasonable blend of user and machine capabilities
 ・allow intuitive modeling while preserving a rigorous formal background
 ・allow for various levels of modelling - from high-level to hard-core
 ・do not try to fully automate everything - understanding of design and problems is necessary

We believe that we achieve this through the combination of a rigid formal background, the incorporation of order-sorted equational theory, an executable semantics via rewriting, high-level programming facilities (inheritance, templates and instantiations, ...), and last but not least a completely freedom to redefine the language of the specification (postfix, infix, mixfix, syntax overloading, ...).

More specifically, the logical foundations are formed by the following four elements:
 ・Order sorted algebras: partial order of sorts
 ・Hidden algebras: co-algebraic methods, infinite objects
 ・Rewriting logic: transitions as first class objects
 ・Order sorted rewriting: executable semantics

(リンク »)

【アクセリア株式会社の研究開発部社員:Norbert Preining氏のコラム】
・第1回:今さら聞けない、機械学習/ディープラーニングとは!? (リンク »)
・第2回:最新の機械学習の代表、ニューラルネットワークとは (リンク »)
・第3回:手書き数字を認識する機械学習 (リンク »)
・第4回:畳み込みニューラルネットワーク (リンク »)
・第5回:機械学習における今後の展開 (リンク »)
・第9回:Analyzing Debian packages with Neo4j (リンク »)
・第10回:Analyzing Debian packages with Neo4j - Part 2 UDD and Graph DB Schema (リンク »)
第11回:Analyzing Debian packages with Neo4j - Part 3 Getting data from UDD into Neo4j (リンク »)

・第6回:アクセリアが手がけるP2P (Peer-to-Peer) (リンク »)
・第7回:効率的な検索を可能にする、グラフデータベース (リンク »)
・第8回:アクセリアにおけるディープラーニング適用例 (リンク »)

関連情報へのリンク »