2013 Fiscal Year Final Research Report
Software Design using Model Cheking
| Project/Area Number |
21500036
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Software
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
OKANO Kozo 大阪大学, 情報科学研究科, 准教授 (70252632)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
谷口 健一 (00029513)
|
|---|
| Project Period (FY) |
2009-04-01 – 2014-03-31
|
| Keywords | モデル検査 / モデル / 形式手法 / 時間オートマトン / CEGAR / OCL / JML |
|---|
| Research Abstract |
This research investigates formal approach on software, especially design of software and its correctness.
The research mainly researches:
1 CEGAR loop algorithm for timed automaton; 2. JML-OCL conversion and its application to open softwares; 3. modelchecing of timed automata and its application to a line tracing robot; 4. JML assertion generation from ordinal program code using mathematical analysis on loop structure; and 5. automatic verification on consistency between equals method and hasCode method in Java programs.
|
