Core Concepts
本論文は、PVS定理証明システムにおける微分動的論理(dL)の正式な埋め込みを提示する。これにより、ハイブリッドシステムの仕様と検証を対話的にPVS内で行うことができる。
Abstract
本論文は、微分動的論理(dL)の形式的な埋め込みをPVS定理証明システムで行った研究について述べている。
主な内容は以下の通り:
dLのハイブリッドプログラムの構文、意味論、論理仕様を形式的にPVSで定義した。これにより、PVS内でハイブリッドプログラムを記述し、その性質を論理的に推論できるようになった。
dLの推論規則をPVSの定理として形式的に検証し、PVSのプローバインターフェースに実装した。これにより、dLスタイルの証明をPVS内で行えるようになった。
PVSの機能を活用して、dLを超えた機能を実現した。例えば、PVSライブラリの既存の定義や数学理論を取り込んだり、ハイブリッドプログラムのメタ的な性質を推論したりすることができる。
提案手法"Plaidypvs"は、NASAのPVSライブラリの一部として公開されており、ハイブリッドシステムの形式検証に活用できる。
Stats
ハイブリッドシステムは安全性や重要性の高いアプリケーションで広く使われている。
微分動的論理(dL)は、ハイブリッドシステムの仕様と推論のための形式的フレームワークである。
KeYmaera XはdLの実装であり、いくつかのサイバーフィジカルシステムの検証に使われている。