Specification and Verification of Software with CafeOBJ - Part 1 - Introducing CafeOBJ

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.

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.

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

Our vision for safety aware software development can be summarized as follows:
　・Step 1: Model and describe a system in order-sorted algebraic specification
　　The domain/design engineers construct proof scores hand-in-hand with formal specification;
　・Step 2: Construct proof score and verify the specification by rewriting
　　The proof scores (CafeOBJ code) are executable instructions, which, when evaluated provide proofs of
　　desirable properties of the specification.

This concludes the first part of this series on CafeOBJ. We will dive into the language of CafeOBJ in the next blog.


■関連ページ
【アクセリアのサービス一覧】
　・サービスNAVI