ソフトウェア設計基礎技術

ソフトウェアを設計・実現したときに,それらがもともとの要求に対して,正しいということをなんらかの方法で確かめておく必要があります.
例えば, 電子商業取引を行うためのソフトウェアや交通制御システムなどの重要性を考えれば,それらの設計や実現の正しさをできるだけ確認しておくことの重要性は明らかでしょう.

ところで, それらが正しいということを確認するには,多くのテストを行うなど,いくつか方法が考えられますが,実際には, どの方法を用いても完全に正しさを確認できたと言えないのが現状です.
この研究では,少しでも,その正しさの確認をより完全なものに近づけるために以下のようなアプローチを研究しています.

それは,作成された設計・実現に対してそれが正しいという条件を表す論理式をつくり, その式が本当に成り立つかを調べるという方法です(論理式が成り立てば, その設計・ 実現が正しいということが数学的に成り立ちます).
この際, そのような論理式は非常に膨大かつ複雑になるので,そのような式の生成や成立するかどうかの検査にコンピュータを使うことになります.

これらの作業は,たとえば,自動車を実際につくる前に,設計図を作成し,そこから, 強度計算, 走行性能計算などをするために,複雑な方程式を作成し,その方程式を解くという作業になぞらえることができます.
対象が,ソフトウェアであることによる大きな違いは,そのような方程式の作成や,解法のうち多くの作業をコンピュータで自動化できるという点です.
ここで問題になってくるのは,解かなくてはいけない式の量が極めて多いこと以上に,「論理式が成立するかどうか」の判定が本質的に計算時間を多く必要とする難しい問題でもあるということです.

最近は, このような問題に対する解決を行うためのさまざまな技法(モデル検査、静的検査、MDA,アサーション)やツールが実用化されつつあります.
われわれはこれらの技法やツールをソフトウェア設計の観点から活用する方法論について具体的な研究をすすめています.

具体的には以下のテーマについて研究を行っています.

実時間システムのモデル検査技法

おもに状態爆発を防ぐためのCEGAR loopについて研究をしています

概要

ソフトウェアを設計・実現したときに,それらがもともとの要求に対して,正しいということをなんらかの方法で確かめておく必要があります.
それらが正しいということを確認するには,多くのテストを行うなど,いくつか方法が考えられますが,実際には, どの方法を用いても完全に正しさを確認できたと言えないのが現状です.

この研究では,少しでも,その正しさの確認をより完全なものに近づけるために次のようなアプローチを研究しています.
それは,作成された設計・実現に対してそれが正しいという条件を表す論理式をつくり, その式が本当に成り立つかを調べるという方法です. この際, そのような論理式は非常に膨大かつ複雑になるので,そのような式の生成や成立するかどうかの検査にコンピュータを使うことになります.
そのような方法のなかで有望な方法の1つがモデル検査技法です。

モデル検査技法は,情報システムを状態遷移モデルとしてモデル化し,作成したモデルが与えられた性質を満たすかどうかをコンピュータを用いて検証する手法です.
モデル検査はシステムの設計段階で適用可能なため,不具合の早期発見に有用であると言えます.また,作成したモデルに対してしらみつぶしに検査を行いますので,一般的なテストなどに比べて検査結果の信頼性が高いことも利点であると言えます.
このような点から,情報システムの高信頼性を実現するため,システム開発にモデル検査を利用することが強く望まれています.

しかしモデル検査ではモデルに対してしらみつぶしに検査を行うため,大規模なシステムに対しては検証コストが爆発的に増加してしまいます.
最悪の場合検証不能となってしまうことがあります(状態爆発).
このような問題に対して,検証したい性質に着目し,検証したい性質と関連の小さい部分を抽象化することでモデルの規模を縮小するモデル抽象化が注目を集めています.

楠本研究室では,実時間的な振る舞いが要求される実時間システムや確率的な振る舞いを持つようなシステムを対象とし,モデル検査を効率的に行う方法について研究を行っています.
扱っているモデルは以下のものが挙げられます.

  • 実時間システムをモデル化する「時間オートマトン」
  • マルコフ決定過程,離散時間マルコフ連鎖,連続時間マルコフ連鎖などの「確率モデル」
  • 実時間的な振る舞い,確率的な振る舞い両方をモデル化する「確率時間オートマトン」

また,確率的モデル検査を応用し,ネットワークシステムの性能評価なども行っています.


以下ではここで挙げた時間オートマトンを対象とした抽象化技術に関する研究について詳しく説明します.

反例に基づく抽象化洗練ループCEGARによる時間オートマトンのモデル抽象化

時間オートマトンは有限状態の状態遷移モデルにクロックと呼ばれる実時間的な振る舞いをする変数を追加したモデルです.時間オートマトンを用いることで交差点の信号機システムのように実時間的な振る舞いをするシステムをモデル化することができます.

しかし,時間オートマトンは実数値をとるクロック変数を持つため状態爆発の問題がより深刻になってしまいます.そこで私たちは時間オートマトンに対するモデル抽象化手法を提案し,状態爆発の問題を改善することに取り組んでいます.具体的には,モデル検査の際に得ることができる「反例」を利用して抽象化されたモデルを洗練することで適切な抽象モデルを生成することができるCEGAR(CounterExample?-Guided Abstraction Refinement)[Clarke]という枠組みを利用して抽象化を実現しています.

  • [Clarke] E. M. Clarke et.al,“Counterexample-guided abstraction refinement for symbolic model checking,” Journal of the ACM, vol.50(5), pp752-794, 2003.

私たちのグループでは,このCEGARの枠組みを利用し,与えれた時間オートマトンが持つクロック変数を全て除去するという抽象化を行い,得られた反例をもとに適切にモデル洗練を繰り返すことでクロック変数を持たない(かつ正しい検査結果を返す)抽象モデルを生成することに成功しました.

代表的な研究成果

  • T. Nagaoka, K. Okano, S. Kusumoto, “An Abstraction Refinement Technique for Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop,” IEICE Transactions on Information and Systems, Special Section on Formal Approach, to appear, 2010.
  • 長岡武志, 岡野浩三, 楠本真二, “時間オートマトンを対象としたコンポーネント部分合成による抽象化洗練手法の改良,” 組込みシステムシンポジウム2008論文集, vol. 2008, no. 9, pp.141-150, 2008.
  • 伊藤明彦, 長岡武志, 岡野浩三, 楠本真二, “確率的モデル検査ツールを用いた実時間ネットワークシステムの検証手法の提案およびネットワークシミュレータNS-2との比較,” 電子情報通信学会技術報告, vol. 109, no. 170, pp. 37-42, 2009.
  • T. Nagaoka, A. Ito, K. Okano, S. Kusumoto, “QoS Evaluation for Real-time Distributed Systems Using the Probabilistic Model Checker PRISM,” Proceedings of the International Workshop on Informatics (IWIN2009),pp. 64-70, 2009.

UML研究グループ

UML記述からのソフトウェア導出に際し、モデル検査、静的検査を活用するための手法についておもに研究しています.

ソフトウェア設計について高位で仕様記述をきちんと記述することが重要となります.またそのためのツールや方法論が様々研究されています.
この研究では主に次の3つの具体的なテーマを扱っています.

OCL JML変換

OCL はUML 記述に対しさらに詳細に性質記述を行うために設計された言語です.より実装に近い面での制約記述言語として,Java プログラムに対してJML (Java Modeling Language) が提案されています.JML,OCL ともにDbC (Design by Contract) の概念に基づきクラスやメソッドの仕様を与えることができます.

この研究ではOCL からJML への変換について研究しています.またこの技術のモデル駆動型開発法への応用も視野に入れて研究を行っています.

論理式学習支援

ソフトウェア設計開発においてフォーマルアプローチが近年注目を浴びています.この技術の基本は数理論理学であり,とりわけ形式証明の概念を理解することは,フォーマルアプローチの基本技術の理解に対して重要です.形式証明の学習は形式体系の重要な概念であるが,厳密な操作を要求されるため初学者に対する敷居は高いと思われます.
そこで,本研究では,学部生の論理学の授業において形式証明の学習を支援するツールの試作と簡単な評価実験行いました.

静的検査可視化ツール

ソフトウェアの品質を調べる手段として単体テストや静的検査などがあります.単体テストの問題点として,テスト仕様書で想定するケースに漏れがある場合はその箇所のテストが行われないため,テスト結果の品質がテストケースに依存することが挙げられます. 一方,プログラムを実行せずにソースコードを検査することを一般に静的検査といいます.
静的検査の問題点として,検査の品質が記述した仕様の質に依存するということや,結果がクラス単位であり,かつテキストで出力されるため,クラス間の呼び出し関係が読み取りにくく,結果が分かりづらいということが挙げられます.
この研究では単体テストおよび静的検査の結果とクラスにおけるメソッド呼び出し情報を用いてこれらの情報を総合的に視覚化することにより,より精緻なソフトウェア品質の情報提供を可能にすることを目標に,重み付き有向グラフを表示するツールをEclipse のプラグインとして試作をしました.また,このツールをJML による仕様が記述された在庫管理プログラムに対して適用し評価を行い,テスト品質および対象ソフトウェアの品質を推定することができました.

代表的な研究成果

  • 尾鷲方志, 岡野浩三, 楠本真二:“在庫管理プログラムの設計に対するJML 記述とESC/Java2 を用いた検証の事例報告”, 電子情報通信学会論文誌, Vol.J91D, No.11, pp.2719-2720 (2008).
  • 尾鷲方志, 岡野浩三, 楠本真二:“メソッドの自動生成を用いたOCL のJML への変換”, 日本ソフトウェア科学会誌コンピュータソフトウェア, Vol. 27, No. 2, to appear, (2010).
  • 宮澤清介, 岡野浩三, 楠本真二: “フォーマルアプローチの基本技術習得のための学習支援システムの試作”, 情報処理学会ソフトウェア工学研究会ワークショップSES2009, ソフトウェアエンジニアリング最前線2009, pp. 69-74 (2009-9).
  • 尾鷲方志, 岡野浩三, 楠本真二: “メソッドの自動生成を用いたOCL のJML への変換 ツールの設計”, 日本ソフトウェア科学会「ソフトウェア工学の基礎」研究会第16 回ワークショップFOSE2009, レクチャーノート・ソフトウェア学35 ソフトウェア工学

アサーション

静的検査の前提となるアサーションの自動導出方法についておもに研究しています.

近年,ソフトウェアは計算機上だけでなく交通機関,銀行システム,自動車や家電などの制御にも使用されており,私達の生活に欠かせないものになっています.そのため,ソフトウェアに不具合があるとその影響は非常に大きなものになります.
よって,開発段階でソフトウェアの不具合を無くすことは非常に重要な問題です.
ソフトウェアの不具合を開発段階で発見し修正することを容易にする技術の一つに,ソフトウェアのソースコード中に”アサーション”と呼ばれる条件式を挿入するというものがあります.アサーションにはソフトウェアが正常に実行されるときに成立すべき条件を記述します.


このアサーションが実行中に満たされない場合,そのソフトウェアには不具合がある可能性があります.また,アサーションを挿入することで不具合の原因箇所の特定が容易になります.しかし,手動でのアサーションの挿入はコストがかかります.そこで,ソースコードにアサーションを自動で挿入する手法の考案,ツールの作成を行っています.

現在は,主に既存Daikonというアサーション生成ツールが出力するアサーションの精度向上について研究しています.Daikonは対象ソフトウェアに対してアサーションを生成する際にそのソフトウェアを実行するための入力データを必要とします.Daikonが生成するアサーションの精度を向上させるには,よい入力データを生成する必要があります.この入力データを生成するために,ソースコードの静的解析ツール,数式処理ツールなどを利用するアプローチで研究を行っています.

代表的な研究結果

  • 堀直哉, 岡野浩三, 楠本真二: “モデル検査技術を用いたインバリアント被覆テスト ケースの自動生成によるDaikon 出力の改善”, 日本ソフトウェア科学会「ソフトウェ ア工学の基礎」研究会第15 回ワークショップFOSE2008, レクチャーノート・ソフト ウェア学34 ソフトウェア工学の基礎XV, pp.41-50 (2008-11).
  • 宮本敬三, 岡野浩三, 楠本真二: “Java に対するループインバリアントを含むDaikon 生成アサーションの妥当性評価”, 電子情報通信学会論文誌, Vol.J91D, No.11, pp.2721-2723 (2008).
  • 宮本敬三,堀直哉,岡野浩三,楠本真二,西本哲:“アサーション動的生成のためのテ ストケース自動生成手法の生成アサーションの妥当性評価”,日本ソフトウェア科学 会「ソフトウェア工学の基礎」研究会第16 回ワークショップFOSE2009,レクチャー ノート・ソフトウェア学35 ソフトウェア工学の基礎XVI,pp.183-190,(2009-11).