| Project/Area Number |
26280019
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Allocation Type | Partial Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Chiba University |
|---|
Principal Investigator |
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
萩谷 昌己 東京大学, 情報理工学(系)研究科, 教授 (30156252)
Artho Cyrille (ARTHO Cyrille) 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (30462831)
山形 頼之 国立研究開発法人産業技術総合研究所, 情報技術研究部門, 主任研究員 (40415758)
田辺 良則 鶴見大学, 文学部, 教授 (60443199)
|
|---|
| Research Collaborator |
KOHAN Alexander 千葉大学
WEITL Franz 千葉大学
MA Lei 千葉大学
SEBIH Nazim 東京大学
|
|---|
| Project Period (FY) |
2014-04-01 – 2017-03-31
|
| Project Status |
Completed (Fiscal Year 2016)
|
| Budget Amount *help |
¥17,160,000 (Direct Cost: ¥13,200,000、Indirect Cost: ¥3,960,000)
Fiscal Year 2016: ¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2015: ¥7,410,000 (Direct Cost: ¥5,700,000、Indirect Cost: ¥1,710,000)
Fiscal Year 2014: ¥5,460,000 (Direct Cost: ¥4,200,000、Indirect Cost: ¥1,260,000)
|
|---|
| Keywords | 実環境モデル検査 / 実行時検証 / ネットワークソフトウェア |
|---|
| Outline of Final Research Achievements |
By fusing runtime verification and model checking, we proposed a framework to verify global specification of network systems with taking account of thread scheduling nondeterminism of the system under test, and implemented its prototype.
Runtime verification alone cannot deal with thread scheduling nondeterminism, and model checking alone cannot handle properties of the whole network system consisting of the system under test and remote peers. By fusing both techniques, we made it possible to detect bugs that cannot be manifested only by existing model checking against the system under test.
|
