HOME | products | LDRA | LDRA_Formal Methods by Stealth


静的解析に活用される形式手法

Formal Methods by Stealth: Formal Methods Implemented
in the LDRA Tool Suite 

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で様々な手法の概説、セクション3で代表的なツール使用法の考察、最後にセクション4でまとめ。
 
2 フォーマルメソッド(形式手法)の技術について
 本来フォーマルメソッド(形式手法)は、仕様やデザインの表記に数学をベースにしたモデルを用いるものとして知られている。Zや有限状態機械(finite state machines(FSMs))など。近年では様々なモデリング手法の使用もフォーマルメソッドとみなされるようになり、この資料にも該当している。そして殆どの手法の主だったベースとなる、コントロールフローモデルとデータフローモデルの2つの基礎となるモデルがある。
 
 ~ <中略> ~