2015 Fiscal Year Final Research Report
Practical model checking for high-performance safety of information control systems
| 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
|
| 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.
|
| Free Research Field |
ソフトウェア工学
|
