03-5211-7750 平日|09:30~18:00

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

           

サービス資料や
ホワイトペーパーはこちら

           資料を【無料】ダウンロードFREE

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

Our vision

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

Norbert Preining

アクセリア株式会社 研究開発部 所属
北陸先端科学技術大学院大学ソフトウェア検証研究センター 研究員
ウィーン工科大学 研究員
Debian開発者
TeX User Group (取締役会員)、Kurt Gödel Society (取締役会員)
ACM, ACM SigLog, 日本数式処理学会、ドイツ数学論理学会
Contact usお問い合わせ

サービスにご興味をお持ちの方は
お気軽にお問い合わせください。

Webからお問い合わせ

お問い合わせ

お電話からお問い合わせ

03-5211-7750

平日09:30 〜 18:00

Download資料ダウンロード

製品紹介やお役立ち資料を無料でご活用いただけます。

Magazineメルマガ登録

最新の製品情報などタイムリーな情報を配信しています。

Free Service

PageSpeed Insights シミュレータ

CDNによるコンテンツの最適化を行った場合のPageSpeed Insightsのスコアをシミュレートしてレポートします。