組み込みソフトへの数理的アプローチ―形式手法によるソフトウェアの仕様記述と検証 (COMPUTER TECHNOLOGY)

著者 :
  • CQ出版
3.50
  • (0)
  • (2)
  • (2)
  • (0)
  • (0)
本棚登録 : 19
レビュー : 2
  • Amazon.co.jp ・本 (247ページ)
  • / ISBN・EAN: 9784789838085

作品紹介・あらすじ

組み込みソフトウェアは年々巨大化し、従来の開発手法では品質が保証できなくなってきています。バグの発生は、ただちにシステムの障害に直結し、社会や人命に重大な損害を与えます。そこで登場した考え方として「形式手法(Formal Method)」があります。数学を基礎とし、プログラムの正しさを証明していこうという考えです。仕様を厳密に定義するための形式仕様記述、モデルの論理的な検証手法である形式検証について、LTSA、Alloy、CBMC、VDMなどの容易に入手できるツールを使いつつ学んでいきます。

感想・レビュー・書評

並び替え
表示形式
表示件数
  • Interface誌の連載をもとにした本で、「形式手法による仕様記述と検証」をテーマとしています。

    いきなり、VDM等が使っている難しい述語論理から始まるのではなく、真理値表や、フィーチャーツリー/原因結果グラフが使っている命題論理から解説されているので読み進めやすくなっています。

    そして、最後には様相論理の一種である時相論理までたどり着く仕掛けです。

    ★★★

    形式手法による仕様記述は、本書に書いてある通り、

     > 自然言語で書かれた「整数を要素とする配列Aの中で最大の要素」を形式的な
     >   | 1 <= x <= n, 1 <= ∀j <= n, A[x] >= A[j] |
     > に置き換えるところがポイント。


    です。
    VDMでは、∀になじみがないプログラマに対してforallで記述できるところが広く受け入れられたのでしょう。

    LTSA, Alloy, CBMC, VDMなどの手に入りやすいツールの使い方についても説明があるので、写経して動かしてみるとよいかもしれません、、、というより、そうしないと理解できないと思いました。

全2件中 1 - 2件を表示

藤倉俊幸の作品

ツイートする