形式手法を試してみよう！

― 信頼性の高いソフトウェアを効率よく開発する手法 ―

2018年7月31日 株式会社 知能情報システム


1. ソフトウェアの検証
それなりに動くコードを素早く書き上げることはできても、それをテスト、デバッグして問題のない コードに仕上げるには相当の手間がかかる場合が多い。いつまでたってもバグが取れない。 不安を抱えながらリリースすることもある。特に、大規模システムや分散システムではアルゴリズムの ロジックが複雑で、どのようなテストをし、またバグが見つかった場合にどのように修正すればよいかを 判断することが難しい。 信頼できるソフトウェアを作る手法には、伝統的な「単体・結合テスト」と、 近年研究が盛んに行われている「形式手法」がある。形式手法は、数理論理学の考え方を取り入れてソフトウェアを 効率よく検査する新しい手法であるが、まだ一般になじみがない。以下に、これらの手法を概観する。


2. 単体・結合テスト
単体・結合テストでは、大きなシステムを小さな部分に分割して検査する。単体テストでは、 分割した小さな部分 (単体) を対象に、それに適当な入出力を与えるプログラム（モック/スタブ）を組み合わせて、 単体の反応が適切か、また単体の内部の変化が適切かといった単体の動きを外と内から見る。 現在、このモック/スタブを作る手段は、各種ソフトウェア開発環境やライブラリで与えられている場合が多く、 いつでも利用することができる。 各単体が検査できたら、次は結合テストを行う。ここでは、テスト済みの各単体のつなぎ目のところで想定した 入出力が行われているか、そして、全体として組み合わせたときに想定した動作が行われているかを見る。 結合テストでは、このようなロジックのテストだけでなく、負荷の対応範囲や処理速度、さらにはセキュリティの テストを行うこともある。


3. 形式手法
単体・結合テストでは、システム（コード）を分割してテストしたのに対し、形式手法ではシステムを抽象化して テストするのが特徴である。大きなシステムの開発では、ＵＭＬの流れ（要件定義、アクティビティ図/ユースケース記述、 モデリング/メッセージチャート、コーディング）に代表されるように、抽象度の高い階層の順に従って設計作業が 進められる（ウォーターフォール・モデル）。形式手法では、直接コードをテストするのではなく、 抽象度の高い階層のシステムの動作を検証したり、抽象度の違う階層のつながり具合を検証したりする。 これにより、早い段階 (例えば、コーディングがなされていないような場合でも) でシステムの不具合が見つかり、 また階層化されたシステム設計の整備を促進して、システム開発の効率化や、保守性を高めてくれる。

形式手法は、モデルチェックと自動定理証明の２つの手法に大別される。モデルチェックは、主に抽象的なシステムの 動作の検証を行う。一方、自動定理証明では、抽象度の違う階層のつながりを検証する。 以下に、これらをもう少し詳しく見てみる。

3-1 モデルチェック
抽象的なシステムの動作を各検証ツールが提供するモデル記述言語で記述し、時相論理にもとづく 要求仕様（例えば、aを入力したら、いつかは b が出力される）を与え、抽象的なシステムの動作がその要求を 満たすかを論理的な演算で自動的に検証する。また要求が満たされない場合は、その原因を出力する。

代表的なモデル検査ツール：SPIN、NuSMV、UPPAAL

3-2 自動定理証明
システム設計の階層で、階層Aが階層Bの抽象化、すなわち階層Bが階層Aの詳細化 (refinement) であるとき、 BがAと矛盾しない詳細化になっているかを自動証明で確かめる。これは大規模なシステムの全体としての整合性を 保証するための重要なステップである。ここでは、AやBの動作モデルが論理式で記述され、BがAをどのように詳細化されたかを 論理式で表現し、その詳細化に矛盾がないかを（自動）定理証明で示す。自動で示せない場合は、その証明を 人がアシストする必要がある。その場合は、どの方向に証明を進めるか、あるいはどの補題を利用するかなどを ツールに教えることになる。

代表的な自動定理証明の検証ツール：Event-B、VDM++


4. 形式手法の長所と短所
長所：
形式手法は、論理に基づく厳密な検証であり、テストケースの抜けが少ない。実際、単体・結合テストで見落とされた バグが形式手法の利用により数多く発見されてきた。また、抽象化されたシステムの検証は、階層化されたソフトウェア設計との 親和性が高く、ソフトウェア設計の整備につながる。そしてその結果、ソフトウェアの保守性、拡張性が容易になる。 また、上流段階での検証を組織的に行えるので、ソフトウェアの開発が効率化される。

短所：
（現段階の）形式手法の検証ツールを使いこなすには、論理式の読み書きの能力が必要になる。 そこに敷居の高さを感じる場合が多い。ただし、その読み書きは決して難しいものではなく、少しの学習で身につく。 決して数理論理学の本などを読む必要はない。一方、形式手法の本質的な問題として、 その手法を実際のソフトウェア開発にどう適用するかの判断が難しい。形式手法の適用ガイドや過去の成功事例などはあるが 、やはりその有効な活用法は対象としているソフトウェアに大きく依存している。形式手法の適用例がまだ十分多くなく、 問題ごとの適用ノウハウが整理されていないのが現状である。


5. 形式手法の適用例と適用ガイド
自動定理証明手法の適用例：
クルーズコントロール(Bosch)、鉄道の制御/信号システム(Siemens Transportation)、 鉄道車両運行量の制御(Newcastle University)、デッドマン装置(AeS)、 パリ地下鉄14号線、鉄道/航空の制御(Systerel)、 水星探査装置の姿勢/軌道制御(Space Systems Finland)、Felica ファームウェア

モデルチェックの適用例：
宇宙機(Deep Space 1: NASA)、エレベーターシステムTWIN、CPU(Intel)、 OS(seL4, INTEGRITY-178B, PikeOS)、コンパイラ(CompCert C compiler)、 その他さまざまな事例

自動定理証明による形式手法は鉄道・航空関係などの大規模システムの効率的な開発で 大きな成果を上げている。一方、モデルチェックの手法は、分散システムや組み込みシステムなどの ロジックが複雑なシステムのバグ検出に威力を発揮している。NASAやIntelは形式手法の専門部署をかかえている。

適用ガイド： 関連情報：

6. どのように形式手法を導入するか？
形式手法は、このように魅力的な長所を備えている。特に、大規模システムや 分散システムの開発でその効果は大きい。しかし一方で、克服すべき短所もかかえている。 形式手法導入のための、現段階での最良の方法は、形式手法を得意とする専門機関に導入と社内教育を 委託することであろう。その中で自社に合った形式手法の適用法をデザインし、その運用方法をアレンジし、 同時に社内教育を実施する。一連のこの大きなルーチンをこなせば、その後の形式手法の適用が円滑に進むはずである。　


免責事項
本稿の情報については十分な注意を払っておりますが、その内容の正確性等に対して一切保証するものではありません。 本稿の利用で生じたいかなる結果についても、当社は一切責任を追わないものとします。

© Copyright 2018, 株式会社 知能情報システム