LDRA 静的解析に活用される形式手法(フォーマルメソッド)でIEC61508、ISO26262 の認証取得を支援

M. A. Hennell1, and M. R. Woodward2
1 LDRA Ltd., Portside, Monks Ferry, Wirral CH41 5LH, U.K.
2 Department of Computer Science, University of Liverpool,
Chadwick Building, Peach Street, Liverpool L69 7ZF, U.K.

　この資料では数学的証明を根拠とするフォーマルメソッド（形式手法）に相当する、様々な静的解析の技術についてまとめている。それら技術は市販される既存ツールである LDRA Testbed によって提供されている。とりわけこのツールは航空機搭載システムの認証取得を目的に多くの顧客にて活用されているが、実はフォーメルメソッド（形式手法）が活用されていることは、あまり知られていない。それはレーダーで監視されないステルス機のように。

キーワード：　フォーマルメソッド（形式手法）；テストツール；静的解析；ソフトウエアのモデリング

1 はじめに
　多くのソフトウエア開発者は、フォーマルメソッド（形式手法）を活用していないと考えている。大抵の場合はその通りであるが、そうでない場合も有る。表面上わからないだけで気付かずに活用している場合があるからだ。この資料でフォーマルメソッド（形式手法）とは、ソフトウエアの全体あるいは一部分のモデルに適応される、数学をベースにした解析テクニックのこと。そして30年以上に渡って良く知られたテストツールに組込まれてきたフォーマルメソッドについて紹介する。またそれらが最も厳しいアプリケーション領域で成果を得ていることから、実践的に活用できるものであることも紹介する。

　LDRA Testbed ツールスイート [1] は、1970年代にテストのカバレッジ尺度 [2]を得るための動的解析ツールを起源としている。そして ADAやアセンブラなど14の異なる言語への対応を経て、静的解析の領域が十二分に拡張された。この静的解析の主だった目的はプログラミングスタンダード違反の検出や、ストロングタイプ（強い型付け）チェックのようなコンストレインツの適応、多くのタイプの欠陥を検出させる強力なアルゴリズムなどに焦点をあわせてきた。この一連の機能を擁するツールを特徴付ける要因の一つは、様々な静的解析が言語の完全なセットに適応され、多くの場合ダイアレクトには依存しないこと。このダイアレクトに依存しないことが、このツールの洗練を象徴する。この資料のセクション２で様々な手法の概説、セクション３で代表的なツール使用法の考察、最後にセクション４でまとめ。

2 フォーマルメソッド（形式手法）の技術について
　本来フォーマルメソッド（形式手法）は、仕様やデザインの表記に数学をベースにしたモデルを用いるものとして知られている。Zや有限状態機械（finite state machines(FSMs)）など。近年では様々なモデリング手法の使用もフォーマルメソッドとみなされるようになり、この資料にも該当している。そして殆どの手法の主だったベースとなる、コントロールフローモデルとデータフローモデルの２つの基礎となるモデルがある。

　～ <中略> ～

日本語版をご請求ください

LDRA ツールスイートの特徴

フローグラフとカバレッジ結果
・あらゆるコンパイラ・実行環境に対応

・静的解析、テストドライバー生成機能、テスト管理機能の融合
　　*システムワイドな静的解析から、テストハーネス、スタブなどを自動生成/ 単体テストのための、コード分析作業を軽減
　　*テストと実行結果は管理され、派生開発などコード変更によるインパクトを自動解析して、テストの再利用を支援

・システムワイドにソースコードを可視化
　　*既存コードを解析し、変更によるインパクトを理解するための情報を、グラフやテーブルを用いて可視化

・動的解析結果をグラフィカルに可視化
　　*フローグラフ・コールグラフ上に、カバレッジ結果をグラフィカルに表示
　　*MCDCカバレッジのコンディションテーブル表示

・IEC61508、DO-178B、MISRA、CERTなど、あらゆるスタンダードに対応
　　*デザインレビューや、要件に対するトレーサビリティなど、開発プロセスの全フェーズのテスト・検証作業の自動化を支援
　　*成果物はエビデンスとして認証機関に提出できるフォーマットに

LDRAの製品情報はこちら