回路デザイン研究室 >> research >> model checking group



形式手法を用いたソフトウェア開発支援

ソフトウェアは社会の重要な役割を担っているため,その信頼性についての要求は日々高まってきています. ソフトウェアの検証にはテストやシミュレーションが用いられてきましたが,ソフトウェアの大規模化・複雑化が進むにつれ,これらの手法には限界が近づいています. そこで,数理的にソフトウェアの正しさを証明する,いわゆる形式手法による検証が求められています.

当研究室では形式手法を用いたソフトウェアの開発支援を目的として,以下のテーマについて研究を行っています.

1) モデル検査を利用するための設計検証支援環境の開発
2) プロセスの双模倣性に基づく設計ドキュメント間の整合性検証
3) UMLを用いたスマートフォンアプリの動作モデル化
4) 有界モデル検査を用いた非同期分散システムの自動検証
モデル検査を利用するための設計検証支援環境の開発

ソフトウェア開発においては,手戻りが開発コストに与える影響が非常に大きく,設計段階での検証が求められています.モデル検査(model checking)は,検査対象となるシステムを状態遷移グラフとしてモデル化し,グラフの網羅的探索によりシステムの正しさを自動検証する手法で,ソフトウェアの開発現場において実用への期待の高い技術です.モデル検査を実装したツールは多くのものが開発されていますが,その利用には専門的な知識が求められることから,普及が十分に進んでいるとは言えません.

当研究室では,設計記述からモデル検査ツールの入力を生成するための検証支援環境を提供することで,開発現場へのモデル検査の普及を目指しています.

  • IPA/SEC 「2013年度ソフトウェア工学分野の先導的研究支援事業」 受託研究, "抽象化に基づいたUML設計の検証支援ツールの開発", 2013.06-2014.02.
プロセスの双模倣性に基づく設計ドキュメント間の整合性検証

大規模なソフトウェア開発プロジェクトでは,単一のソフトウェアに対して繰り返し設計ドキュメントが作成されます.ドキュメントに記述されている内容同士に食い違いがあった場合,その後の開発工程で重大なバグが発生する危険性が高まります.これを防ぐために入念なレビューが行われますが,ソフトウェアの振る舞いに関する部分についての誤りを人の目で発見することは非常に困難です.

当研究室では,ソフトウェアの振る舞いをプロセス代数と呼ばれるモデルで表現し,設計ドキュメント間の整合性をプロセス等価性として定義することで,ドキュメント間の整合性を証明する手法について開発を行っています.

  • H. Miyazaki, T. Yokogawa, et al., "Synthesis and Refinement Check of Sequence Diagrams," IEICE Trans. on INF. & SYST., 2012.
  • T. Yokogawa, S. Amasaki, et al., "Consistency Verification of UML Diagrams based on Process Bisimulation," In Proc. of PRDC2013 (Fast Abstract), 2013.
UMLを用いたスマートフォンアプリの動作モデル化

スマートフォンやタブレット端末の普及により,それらの上で動作するスマートフォンアプリも急激に増加しています.スマートフォンアプリは生活に深く浸透し,その多くは個人情報を扱うことから,アプリの信頼性の向上が強く求められています.ここで,ソフトウェアの高信頼化を目的とした技術は,モデル検査や自動テスト生成をはじめとして数多くのものが提案されていますが,これらを効果的に利用するためにはアプリのモデル化が必要となります.

当研究室では,アプリの振る舞いをUMLの状態マシン図によってモデル化することで,モデル検査による検証やテストケースの自動生成を行う手法について開発を行っています.

  • 落水, 横川ほか: "状態マシン図を用いたスマートフォンアプリのモデル化," 信学技報, SS2013-21, 2013.
有界モデル検査を用いた非同期分散システムの自動検証

ネットワークコンピューティングや大規模非同期回路などの非同期分散システムは,その非同期性とリアルタイム性から設計は非常に困難となります.このようなシステムを解析するために,分散システムのモデルであるペトリネットに時間要素を加えて拡張した時間ペトリネットによるモデル化が用いられています.

当研究室では,有界モデル検査を用いて時間ペトリネットでモデル化された非同期分散システムの検証を行う手法について開発を行っています.

  • 河村, 横川ほか: "SMTソルバを用いた時相ペトリネットの形式的検証," ソフトウェア信頼性研究会第8回ワークショップ(FORCE2012), 2012.






TOP