2013 Fiscal Year Annual Research Report
モデル検査技術を活用したソフトウェア設計方法に関する研究
| Project/Area Number |
21500036
|
|---|
| Research Institution | Osaka University |
|---|
Principal Investigator |
岡野 浩三 大阪大学, 情報科学研究科, 准教授 (70252632)
|
|---|
| Project Period (FY) |
2009-04-01 – 2014-03-31
|
| Keywords | モデル検査 / ソフトウェア / モデル / フォーマルアプローチ |
|---|
| Research Abstract |
ソフトウェアのモデル検査技術の応用として次の研究を行い, 発表した. 1. データベースのスキームの整合性検査，2．プログラムのループのインバリアント自動導出の精度あげるために数理解析ツールを活用する方法, JavaのequalsメソッドとhashCodeメソッドの整合性をSMTソルバーを用いて自動検証する方法．またJML, OCL相互自動変換ツールとそのオープンソフトウェアへの適用や表明カバレッジメトリクスのアイディアについて国際会議等で発表した．１についてはAlloy Analyzerを用いてフォーマルに検証する技法を用いている．2についてはMathematicaを利用することにより精度向上をめざした．3については限定モデル検査やモジュール検証の技法やZ3のビット演算機能を用いて実用的な部分クラスについて自動検証を可能とした．
またプログラムの表明導出，Alloyを用いたプログラム仕様検証，ライントレースロボットの自動検証, JML-OCL自動変換などの論文を掲載した．
|
| Current Status of Research Progress |
Reason
25年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
25年度が最終年度であるため、記入しない。
|
Research Products
(19 results)
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
[Presentation] ウィンターワークショップ2013・イン・那須報告2013
Author(s)
野田夏子, 岡野浩三, 早水公二, 戸田航史, 上野秀剛, 石尾隆, 林晋平, 妻木俊彦, 中村匡 秀, 岸知二, 本橋正成, 鷲崎弘宜
Organizer
情報処理学会研究報告
Place of Presentation
東京
Year and Date
20130710-20130710
