|
本年度は、19年度のステートチャートの構造の抽象化精錬検証方式の開発と実装及び時間ステートチャートの構造と時間の抽象化精錬検証方式の開発と実装、20年度のリアルタイムオブジェクト指向言語の設計とその検証方式の開発を受けて、オブジェクトが生成消滅するシステムの抽象化精錬で直接に検証できる、動的リアルタイムCEGARの開発と実装に取り組んだ。
その結果、動的リアルタイムCEGARの実現により、オブジェクトの生成消滅といった構造の変化及びリアルタイム性を同時に抽象化精錬して、リアルタイムオブジェクト指向システムの効率的なモデル検査が実現できることを明らかにした。
これは、リアルタイムシステムの効率的な検証方式の実現可能性を実証したばかりではなく、広くオブジェクト指向システムの効率的な検証方式の実現可能性を実証しており、Javaなどのオブジェクト指向言語で記述されたインターネット上のソフトウェアの効率的な検証方式の実現可能性を示唆しているといった重要な意義のあるものである。
来年度は、本研究の成果を広く適用させるために、広くオブジェクト指向システムの効率的な検証方式の解明に取り掛かる予定である。
|
