ソフトウェア(論理構造物)の検証

情報システム学科 
教授 深海 悟

深海 悟
  • 自動販売機の概略状態遷移 自動販売機の概略状態遷移

    自動販売機の概略状態遷移

物理構造物

人類は有史以来様々な道具、機械、建造物を作ってきました。これらの多くは物理構造物であり、現在では物理学(力学、電磁気学等)と微積分学が基礎となって作られているのは周知の事実です。

もう少し具体的に説明すると、建造物や機械、電気回路等においては、作ろうとするものが満たすべき機能・性能・制約条件に基づき設計を行います。出来上がった設計がこれら条件を満たしているか否かは、通常は物理学に基づいて検証可能です。そして問題ないことが確認された仕様に基づき、適切なプロセス管理のもとで施工・制作・実装が行われます。できあがった「モノ」が仕様を満たしているかは、理論的に検証できるとは限りませんが、様々なテストで確認できます。

ソフトウェア - 論理構造物

一方、ソフトウェアは物理構造物ではなく論理構造物です。したがって物理学や微積分学ではなく数理論理学が基礎となっています。しかしながら、ソフトウェア開発においては、通常「仕様書」は作成しますが、仕様に論理的な問題がないかの確認は関係者が集まって行うレビュー等による場合が多く、数理論理学の道具を使い理論的に検証するといったことは従来あまりなされていませんでした。これは例えてみれば建造物を構造力学の知見を使わずに経験と勘にたよって開発する状況に近いと言えます。もちろん微積分学や構造力学が存在していなかった1000年以上も前に五重の塔のようなすぐれた建造物が作られたのと同じように、経験と勘で優れたソフトウェアが多数作られてきたのも事実です。

とはいえ、いわゆるセーフティクリティカルシステム(障害が起きると人間に危害が及ぶ可能性のあるシステム)に組込まれるソフトウェアが増加している昨今、このような状況を放置することはできず、仕様に問題がないかを厳密に検証したり、その仕様に基づいて開発されたプログラムと仕様に齟齬がないかを厳密に確認する技術の必要性が高まっています。

そこで、数理論理学を基礎とし、数学的に厳密な手法を用いてソフトウェアを開発する方法(フォーマルメソッド)が開発されてきました。ここでフォーマルメソッドとは1つの方法論ではなく、さまざまな手法の総称です。具体的には、ソフトウェアの仕様を自然言語や意味が厳密に定義されていない図で記述するから誤解が生じバグが発生するとの認識のもと、意味が数学的に厳密に定義された人工の仕様記述言語で仕様を記述するもの、さらには、仕様が要求を満たしているか否か、あるいは望ましくない動作を引き起こすことはないかを論理的に検証するもの、出来上がったソフトウェアが仕様を満たしていることを数学的に証明するものなど様々な手法が開発されてきています。ここでは、フォーマルメソッドの中でも比較的とっつきやすいとされる「モデル検査」と呼ばれる技術を簡単に紹介したのち、当研究室で行った研究について紹介します。

モデル検査とは?

ソフトウェアに限らずコンピュータの世界には動作仕様が「状態遷移」で定義できるものがたくさんあります。例えば論理回路(順序回路)の動作、通信プロトコルの振舞いなどは状態遷移としてその仕様を定義することができます。また、特に組込みソフトウェアの場合、その動作仕様を状態遷移として定義できるものが多数あります。さらにはプログラムの動作そのものも、次に実行する命令の行番号とその時点での変数の値で1つの状態を定義すれば、命令の実行は状態遷移としてとらえることができます。

モデル検査とは、状態遷移が所望の性質を満たしているかを全自動でチェックする技術です。これはテストとは異なり、サンプル的にいくつかの状態遷移系列(以下パスと呼びます)だけをチェックするのではなく、存在しうる全てのパスについて網羅的にチェックします。また、与えられた性質を満たしていない場合は、満たしていないパスを具体的に提示することが可能で、不具合箇所の特定に大きな情報を提供してくれます。存在しうる全てのパスをチェックすることから、状態空間が無限の場合には適用できません。実際、通信プロトコルの仕様やプログラムの状態空間は一般には無限空間となるため、モデル検査を単純には適用できませんが、無限空間を有限空間に押し込む工夫(これを抽象化と言います)をすれば適用できます。
また、上記で「所望の性質」と述べましたが、モデル検査では通常、「時相論理」と呼ばれる論理の論理式で検証したい性質を表現します。ここでは専門的になりすぎるので時相論理の話は割愛しますが、プログラムの仕様記述や検証の分野ではよく用いられる論理体系です。検証できる性質(=時相論理式で記述可能な性質)は、通常の言葉で表現すると以下のようなものです。
例えば複数のプロセスが同時並行的に動作しているシステムにおいて、

・デッドロックに陥ることはない
・複数のプロセスが共有リソースをアクセスする権利を同時に獲得することはない
・すべてのプロセスがいずれは望ましい状態に到達することができる
・すべてのプロセスが公平に実行される 等。

モデル検査では、設計仕様に基づいて生成される状態遷移を専用の言語で記述し、満たしてほしい性質を時相論理式で記述すると、あとは全自動で検証し、満たしていない場合はその反例を提示してくれます。したがって、設計段階で仕様の正しさを厳密に検査することが可能で、最近では特に組み込みソフトウェアの開発現場等で使用されるようになってきています。

なお、コンピュータサイエンス分野の様々な領域で時相論理が有効に活用できることを最初に示したA. Pnueli、モデル検査の概念を最初に提案したE. M. Clarke達がそれぞれ相次いでチューリング賞(コンピュータサイエンス分野では最も権威あるとされている賞)を受賞していることからも、この技術の重要性がうかがえます。

当研究室では、モデル検査技術について様々な研究を行ってきましたが、そのうちの一つにC言語プログラムにおける配列の範囲外参照の可能性を検出し修正提案を提示するシステムの開発があります。Cのプログラムでは実行中に配列の範囲外参照を行ってしまうというバグがよく問題になります。これはある特定の条件が重なったときのみ発生する場合が多く、原因を突き止めるのが難しいバグの一つです。そこで、プログラムのソースコードを対象としたモデル検査により範囲外参照が起きる可能性をチェックし、可能性がある場合には、モデル検査の反例とソースコードの解析により、どのようにプログラムを修正すれば範囲外参照を回避できるかを提示してくれるシステムを提案しました。この研究は、情報処理学会で発表したところ高く評価され、発表した古川直樹君が情報処理学会推奨修士論文の認定を受けました。

ページの上部へ

大阪工業大学