ディペンダブルソフトウェア工学中島研究室

プロジェクト

最近、行っている研究テーマと産学連携の活動を紹介します。

モデリングや要求仕様などソフトウェアの開発上流工程での形式手法利用に関わる研究

Event-B振る舞い仕様の自動検証
- 複数のイベント連鎖からなる振る舞い仕様をロジック・モデル検査の方法で検証
- 抽象化技法（述語抽象，ランキング抽象）の良い応用例
- 教科書「形式手法入門」（オーム社2012）でも説明に使用
フィーチャダイアグラムの形式化と自動検査
- ソフトウェア・プロダクトライン工学（SPLE）で用いるフィーチャダイアグラムの命題論理による形式化
- Alloyを用いた制約充足性解析の方法
- 制約充足しないフィーチャダイアグラムの不具合個所を発見する自動解析アルゴリズム
- 以上の基本方式を実現したGUIベースツール FDChecker
UML/OCLの形式化と自動検査

Ｃ言語等で書かれたプログラムを対象とした検査の自動化に関する研究

Design-by-Contractを利用したモジュラー検証法と有界モデル検査の統合
- 関数ポインタを含むDesign-by-Contract（DbC）の導入
- 有界化に伴う近似の検査結果への影響をテスト自動生成の方法で補完
- 橋本祐介（総研大博士課程）：SES2011最優秀論文賞受賞
プログラム仕様からのテストケース自動生成
- 劉少英先生（法政大学）との共同研究
プログラムの自動デバッグ
- プログラム不具合個所の自動発見
- フィーチャダイアグラムの不具合個所自動発見ならびにＣプログラムの有界モデル検査の研究から出発
- プロジェクトCBEL:細部博史先生（法政大学）ならびにM. Rueher先生（ニース大）との共同研究

ロジック・モデル検査に代表される自動検証アルゴリズムをソフトウェア工学の諸側面に応用する研究

SMTツールの開発とオブジェクト指向デザイン自動解析への応用
- 構造的な仕様（オブジェクト図）と振る舞い仕様（状態遷移図）を統合したデザイン記述にロジック・モデル検査の方法を適用
- 専用の有界検査ツールをOpenSMTの拡張として開発
モデル検査によるWebサービス記述の振る舞い検証
- SPINを用いたWSFLおよびWS-BPELの振る舞い検証（2006年頃まで実施）

要求や高位ポリシーの破れを実行時に監視し不具合に対応する自己適応システム（Self-* Systems）の構成法ならびに当該システムが持つ性質に関する研究

制御対象と制御系の双方が複雑に絡み合うCPS (Cyber-Physical Systems)型組込みシステムを対象としたモデリングおよび自動検証に関する研究

産業界６社（NTTデータ、富士通、NEC、日立、東芝、SCSK）との形式手法の実践に関する研究開発

SSR（産学戦略的研究フォーラム）2010・2011年度採択調査研究テーマ

（研究代表者としての受け入れ）