|
| 2012年度 パッヘ研究奨励金Ⅰ-A-２（特定研究助成・一般）研究成果報告書 |
|
| 氏名 |
張 漢明 |
所属 |
情報理工学部ソフトウェア工学科 |
| 研究課題 |
並行システム記述におけるフォールトパターンに関する研究 |
|
| 研究実績の概要 |
マルチコアプロセッサの出現や分散システムの普及に伴い，並行プログラミング技術の重要性が注目されている．並行システム記述の検証に対してモデル検査の有用性が報告されている．モデル検査ではシステムが満たすべき性質の真偽を自動で判定し，その結果が偽の場合は反例を出力する．反例からシステム記述の誤りを特定することは本質的に困難な作業であり，検証にかかるコストが高くなる要因の1つである．
本研究の目的は，並行システム記述における典型的なフォールトを自動的に検出する手法を確立することである．反例からフォールトを特定するには，反例の情報から各プロセスの振舞いを抽出し，それぞれ仕様を満たしているか調べる必要がある．検証者の不注意な誤りなどで複数のフォールトが含まれていた場合や，仕様が間違っている場合，フォールトを特定する作業は更に困難なものとなる．事前に典型的な誤りを検出することができれば，検証コストの削減に寄与する事が期待できる．
本研究では，並行システムにおける既知の相互排除問題を分析し，典型的な誤りのパターンを正規表現で表現することにより，誤りの検出を有向グラフのパターン照合問題に帰着することにより問題解決を図った．パターンを用いてフォールトを定義することにより，システム記述の意味を分析するのではなく，構文レベルの解析でフォールトを検出することを可能にする．また，既知の知見からの理論的な分析及び実際の開発事例における誤りの収集を行い，フォールトパターンの有効性を確認するためのツールの試作を行った．
具体的な成果として，（1）典型的なフォールトパターンの分析，（2）事例からのフォールトパターンの抽出，（3）フォールトパターン検出ツールの試作，が挙げられる．典型的なフォールトパターンの分析では，既存の並行システムに関する文献を調査して，正規表現を用いてフォールトを分類した．事例からのフォールトパターンの抽出では，プリンタシステムと自動販売機システムの設計を行い，その過程で起こった誤りを抽出して，フォールトパターンを提示した．フォールトパターン検出ツールの試作では，状態遷移図からCSP記述への変換，CSP記述から軌跡のグラフへの変換，グラフから軌跡の検出ツールの試作を行い，事例で起こった誤りを本試作ツールで検出することを確認した．今後の課題として，フォールトパターンの洗練及び検出ツールの効率化が挙げられる．
|
|
|
| 「雑誌」の部 |
「図書」の部 |
| ① |
論文題目 |
パターンを用いたフォールトの検出に関する考察 |
① |
書名 |
|
| 雑誌名 |
ソフトウェア・シンポジウム 2012 論文集 |
論文名 |
|
| 巻号 |
|
出版社 |
|
| 発行年月 |
2012/06 |
出版年月 |
|
| ページ |
|
ページ |
|
| 著者名 |
張 漢明，野呂 昌満，神谷 浩翔 |
著者名 |
|
| 備考 |
|
備考 |
|
| ② |
論文題目 |
並行システム記述におけるフォールトパターンに関する考察 |
② |
書名 |
|
| 雑誌名 |
電子情報通信学会技術研究報告ソフトウェアサイエンス研究会 |
論文名 |
|
| 巻号 |
Vol. 112，No. 275，SS2012-39 |
出版社 |
|
| 発行年月 |
2012/11 |
出版年月 |
|
| ページ |
p. 35-40 |
ページ |
|
| 著者名 |
張 漢明，野呂 昌満，他 |
著者名 |
|
| 備考 |
|
備考 |
|
| ③ |
論文題目 |
アーキテクチャ指向開発における形式手法の適用に関する考察 |
③ |
書名 |
|
| 雑誌名 |
情報処理学会研究報告, 組込みシステム研究会 |
論文名 |
|
| 巻号 |
2013-EMB-28(11) |
出版社 |
|
| 発行年月 |
2013/03 |
出版年月 |
|
| ページ |
pp. 1-6 |
ページ |
|
| 著者名 |
張 漢明，野呂 昌満，他 |
著者名 |
|
| 備考 |
|
備考 |
|