Specification and Verification of Software with CafeOBJ - Part 1 - Introducing CafeOBJ
Overview on the blog series
・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?
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
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
・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
サービスにご興味をお持ちの方は
お気軽にお問い合わせください。
Webからお問い合わせ
お問い合わせお電話からお問い合わせ
平日09:30 〜 18:00
Free Service