無限小プログラミングによるハイブリッドシステムの形式検証手法

点击翻译按钮获取中文摘要

前年度に提案した無限小プログラミングのための検証のフレームワークに基づいて無限小プログラムのホーア論理に基づく検証手法を提案し実装した．本実装は (1) バックエンドにおいて既存の自動定理証明器を拡張なしに用いることができるという点 (2) 既存研究でソフトウェアのための形式検証手法として提案された手法をそのまま用いることができる点に特徴がある．本研究は，ハイブリッドシステムの検証手法として無限小プログラミングの枠組みを利用するための重要なステップである．提案手法の理論的枠組と本実装に基づく実験結果を論文にまとめ，コンピュータを用いた検証に関する国際会議会議 (CAV) において発表した．また，前年度まで手続き型言語として定式化されていた無限小プログラミングをストリーム処理言語に拡張した言語（超準ストリーム言語）の基礎づけと検証の研究を行った．ストリームは電気信号等により近い表現を持つため，本研究によってハイブリッドシステムの開発現場で用いられている設計図に直接形式検証を適用することが将来的に可能になると期待される．理論的にも (1) 超準化されたストリームと連続的な信号との関係 (2) 超準ストリームプログラムの不動点意味論 (3) 連続的信号を演繹的な検証手法である型システムで検証するための手法といった興味深い展開が見られている．本研究の内容を論文にまとめ，プログラミング言語の原理に関する国際会議 (POPL) において発表した．