| Project/Area Number |
25330075
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Ibaraki University |
|---|
Principal Investigator |
|
|---|
| Research Collaborator |
TAKEZAWA Takayuki (株)日立製作所, インフラシステム社
YAMAGATA Tomoyuki (株)日立製作所, インフラシステム社
|
|---|
| Project Period (FY) |
2013-04-01 – 2016-03-31
|
| Project Status |
Completed (Fiscal Year 2015)
|
| Budget Amount *help |
¥3,770,000 (Direct Cost: ¥2,900,000、Indirect Cost: ¥870,000)
Fiscal Year 2015: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2014: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2013: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
|
|---|
| Keywords | モデル検査 / モジュラ検証 / ソフトウェア安全性検証 / 情報制御システム / 機能安全 / モデル駆動開発 |
|---|
| Outline of Final Research Achievements |
This study developed stepwise model checking techniques based on the domain-specific properties of the information control system. This method can verify the model with less memory and shoter period of time in a more large-scale model than the conventional method. Next, this study proposed a divided model checking technique that allows the checking of model by the system division. This method can achieve model checking without losing the interrelationship of the divided sub-systems in a shorter time than non-dividing.
In addition, this study has devised a modular verification approach to solve the drawbacks of the two methods. This approach enable modular model checking by the module division of the 3 types which are physical divisions of the dilute cause-and-effect relationship, divisions in the structural symmetry, divisions of the highly independent behavior. The effect of this approach can be determined by ratio of number of independent attributes and common ones.
|
