大阪大学　数理・データ科学教育研究センター
Center for Mathematical Modeling and Data Science,Osaka University

超準解析による物理情報システムの形式検証―離散から連続・ ハイブリッドへ
Nonstandard Analysis and Formal Verification of Cyber-Physical Systems: From Discrete to Continuous and Hybrid Dynamics

蓮尾一郎 (東京大学大学院情報理工学系研究科)

1. ホーム
2. セミナー・集中講義
3. セミナー
4. 超準解析による物理情報システムの形式検証―離散から連続・ ハイブリッドへ
   Nonstandard Analysis and Formal Verification of Cyber-Physical Systems: From Discrete to Continuous and Hybrid Dynamics

大阪大学 数理・データ科学セミナー　数理モデルセミナーシリーズ第2回

超準解析による物理情報システムの形式検証―離散から連続・ ハイブリッドへ
Nonstandard Analysis and Formal Verification of Cyber-Physical Systems: From Discrete to Continuous and Hybrid Dynamics

蓮尾一郎 (東京大学大学院情報理工学系研究科)

自動車や飛行機，プラントといった，コンピュータ制御される物理システム（物理情報システム）は現代社会のあらゆるところに存在し，それらの品質保証は重要な問題である．これらのシステムは，デジタル・離散的な動作（コンピュータ制御ゆえ）と，アナログ・連続的な動作（物理系ゆえ）の両方を持ち，それゆえ
ハイブリッド・システムとも呼ばれる．

ハイブリッド・システムの研究には，制御理論（もともと連続）と，計算機科学（もともと離散）の2つのアプローチがあるが，本発表では超準解析を用いて離散的な理論体系を「文字通りそのまま」ハイブリッド・システムに移転する手法を紹介する．具体的には，while ループを持つ命令形プログラミング言語に無限小を表す定数 dt を導入し，連続ダイナミクスをも whileループで表現できるようにした上で，ホーア論理とよばれるプログラム検証手法を適用しハイブリッド・システムの性質を証明する．この論理的検証手法の健全性は，超準解析を用いたプログラム意味論の上でLo´s の定理や移転原理を用いることで証明される．

この手法に基づいて実装した自動検証器や，抽象解釈による到達可能性解析器，また，ハイブリッド・システムの設計の現場で使われるものにより近い形式化（ハイパーストリーム処理系）についても述べる．