|
| 2013年度 パッヘ研究奨励金Ⅰ-A-２（特定研究助成・一般）研究成果報告書 |
|
| 氏名 |
張 漢明 |
所属 |
情報理工学部ソフトウェア工学科 |
| 研究課題 |
アーキテクチャ指向開発における実行前検査および検証支援に関する研究 |
|
| 研究実績の概要 |
| |
組み込みシステムの大規模化および複雑化，マルチコアプロセッサの出現，ウェブサービスに代表される分散システムの普及に伴い，並行プログラミング技術の重要性が注目されている．並行システムの記述をレビューやテスティングで検証することは本質的に困難な作業であり，形式手法による検証支援技術の導入が期待されている．
本研究の目的は，信頼性およひ安全性の高いソフトウェアの開発を効率良く支援するために，アーキテクチャ指向ソフトウェア開発における形式手法に基づいた実行前検査および検証支援手法を提案することである． プログラミングにおけるデバッグ作業の困難さと同様に，アーキテクチャの検証においても並行システム記述のフォールトの特定は，困難な作業である．アーキテクチャ段階における記述モデルを分析して，仕様に対する正当性検証の手法を提示するとともに，その誤りを分析してパターンとして定式化することにより検証の支援を図った．
本研究では，アーキテクチャ段階での振る舞い記述をイベントの送受信に限定することにより，アーキテクチャ記述の抽象化を図るとともに，アーキテクチャ段階での段階的な詳細化を検討した．詳細化関係を差分で記述することにより，詳細化関係の追跡性と保守性を容易にした．また，誤りの分析では，仕様に対する誤りを形式的に表現して，誤りの情報を付加することにより，フォールト特定の支援を図った．
具体的な成果として，（1）際どい実行順序を考慮した検証手法の提示，（2）階層モデルにおける検証手法の提示，（3）フォールトパターンの導出手法の提示，が挙げられる．際どい実行順序を考慮した検証手法では，複数からの同時入力を考慮した設計・検証方法を提示した．同時性を考慮しない単純な非同時モデルから，同時性を考慮対応した同時モデルを差分として設計・検証する方法を与えた．階層モデルにおける検証手法では，システムを論理モデルと物理モデルに階層化し，モデル間のプロトコルを基準とした検証条件を提示した．モデル間のプロトコルを明示することにより，検証をモデル毎に分割する手法を与えた．フォールトパターンの導出手法では，実行順序の正規表現に対して，その誤りを形式的に導出する方法を提示した．仕様に対する誤りの箇所を指摘することにより，フォールト特定の支援を図った．今後の課題として， 事例の開発を通して本手法の有効性の検証と洗練を図ることがあげられる．
|
| |
|
|
| 「雑誌」の部 |
「図書」の部 |
| ① |
論文題目 |
際どい実行順序を考慮した並行システム検証に関する考察 |
① |
書名 |
|
| 雑誌名 |
情報処理学会研究報告，組み込みシステム研究会 |
論文名 |
|
| 巻号 |
2014-EMB-32(8) |
出版社 |
|
| 発行年月 |
2014年3月 |
出版年月 |
|
| ページ |
pp.1-6 |
ページ |
|
| 著者名 |
張漢明，沢田篤史，野呂昌満 |
著者名 |
|
| 備考 |
|
備考 |
|
| ② |
論文題目 |
パターンを用いたフォールト検出 |
② |
書名 |
|
| 雑誌名 |
ワークショップ：プログラム・デバッグ自動化の現状と今後（ソフトウェアエンジニアリングシンポジウム2013） |
論文名 |
|
| 巻号 |
|
出版社 |
|
| 発行年月 |
2013年9月 |
出版年月 |
|
| ページ |
|
ページ |
|
| 著者名 |
張漢明，野呂昌満，沢田篤史 |
著者名 |
|
| 備考 |
|
備考 |
|
| ③ |
論文題目 |
|
③ |
書名 |
|
| 雑誌名 |
|
論文名 |
|
| 巻号 |
|
出版社 |
|
| 発行年月 |
|
出版年月 |
|
| ページ |
|
ページ |
|
| 著者名 |
|
著者名 |
|
| 備考 |
|
備考 |
|