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
|
| Project Status |
Completed (Fiscal Year 2013)
|
| Budget Amount *help |
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2013: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2012: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2011: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2010: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2009: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
|
|---|
| Keywords | モデル検査 / モデル / 形式手法 / 時間オートマトン / CEGAR / OCL / JML / ソフトウェア / フォーマルアプローチ / モデル駆動開発 / 表明 / CEGAR LOOP / 確率時間オートマント |
|---|
| 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.
|
Report
(6 results)
Research Products
(98 results)
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
[Presentation] ウィンターワークショップ2013・イン・那須報告2013
Author(s)
野田夏子, 岡野浩三, 早水公二, 戸田航史, 上野秀剛, 石尾隆, 林晋平, 妻木俊彦, 中村匡 秀, 岸知二, 本橋正成, 鷲崎弘宜
Organizer
情報処理学会研究報告
Place of Presentation
東京
Related Report
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
