| 研究課題/領域番号 |
26280019
|
|---|
| 研究種目 |
基盤研究(B)
|
| 配分区分 | 一部基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
ソフトウェア
|
|---|
| 研究機関 | 千葉大学 |
|---|
研究代表者 |
山本 光晴 千葉大学, 理学(系)研究科(研究院), 准教授 (00291295)
|
|---|
| 研究分担者 |
萩谷 昌己 東京大学, 情報理工学(系)研究科, 教授 (30156252)
Artho Cyrille 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (30462831)
山形 頼之 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (40415758)
田辺 良則 鶴見大学, 文学部, 教授 (60443199)
|
|---|
| 研究協力者 |
コハン アレクサンダー 千葉大学
ヴァイテル フランツ 千葉大学
馬 雷 千葉大学
セビ ナジム 東京大学
|
|---|
| 研究期間 (年度) |
2014-04-01 – 2017-03-31
|
| キーワード | 実環境モデル検査 / 実行時検証 / ネットワークソフトウェア |
|---|
| 研究成果の概要 |
実行時検証とモデル検査とを融合させることにより、ネットワークシステムが全体としての仕様を満たすことを検証しつつ、それが検査対象プログラムのスケジューリングによらないことを検査するような枠組を提案し、そのプロトタイプを実装した。
実行時検証単独では検査対象のスレッドスケジューリングに依存する挙動の違いを捕えられず、モデル検査単独ではネットワークシステム全体として満たして欲しい性質と直接に結びつかない。両者を融合させることにより、検査対象プログラムに対する原始的な性質のモデル検査では顕在化しないようなバグを検出可能にする。
|
| 自由記述の分野 |
情報数理学
|
