2018 Fiscal Year Annual Research Report
Research on Highly Reliable Agile Formal Engineering Methods
| Project/Area Number |
26240008
|
|---|
| Research Institution | Hosei University |
|---|
Principal Investigator |
劉 少英 法政大学, 情報科学部, 教授 (90264960)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
児玉 靖司 法政大学, 経営学部, 教授 (30266910)
緒方 和博 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (30272991)
|
|---|
| Project Period (FY) |
2014-06-27 – 2019-03-31
|
| Keywords | アジャイル開発 / 形式工学手法 / 仕様アニメーション / テストに基づく形式検証 / モデル検査 / 形式仕様に基づくテスト / 形式仕様記述手法 |
|---|
| Outline of Annual Research Achievements |
本年度の研究では、次の活動に集中して努力してきた。
（１）自動テストに基づくアルゴリズム関数定理の形式検証理論と技術の確立。アジャイル形式工学手法を実現するためには、形式仕様に基づくプログラムの自動検証が不可欠である。従来のホーア論理によりプログラムの正しさの検証技術ではバグがあるプログラムに対応し難いし、自動化もほとんど不可能である。本研究では、形式仕様に基づく自動テスト技術とホーア論理を適切に統合して、プログラムの正しさを自動的に検証する理論と手法を確立した。但し、現在の手法では、基本データ型のみを使用するプログラムに限られており、複合データ型の対応には課題がまだ残っている。（２）形式仕様のシステムレベルの一致性を検証するために、形成された論理式のテストプロセスのアニメーション手法と支援ツールの開発。この中で、有効なテストデータの自動生成支援ツールと論理式のアニメーション支援ツールの研究が含まれている。（３）プロセス仕様のアニメーションのために、入出力を表すGUIの自動生成する支援ツールの開発。SOFL仕様記述言語の様々なデータ型を対応するプロセスの入出力のGUIを自動的に生成するプロトタイプが開発された。これによって形式仕様の分かりやすいアニメーションを実現できる。（４）モデル検査プロセスのアニメーション技術を確立、プロトコールの性質の形式検証に適用、その効果を調べた。（５）SOFL仕様記述言語に基づくアジャイル形式工学手法のフレームワークを確立、その中の各段階の技術の協力関係と役割を明らかにした。（６）研究成果を反映する多数の論文を作成し、ACM Transactions on Software Engineering MethodologyやIEEE Transactions on Software Engineeringなど論文誌と国際会議に投稿又は公表した。
|
| Research Progress Status |
平成30年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
平成30年度が最終年度であるため、記入しない。
|
