MMDS大阪大学 数理・データ科学教育研究センター
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

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

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

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

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

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

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

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

講師: 蓮尾一郎 (東京大学大学院情報理工学系研究科)
テーマ: 大阪大学 数理・データ科学セミナー 数理モデルセミナーシリーズ第2回
日時: 2015年06月12日(金) 16:45-17:45
場所: 大阪大学 豊中キャンパス 基礎工国際棟シグマホール
参加費: 無料
アクセス: 会場までのアクセスは下記URLをご参照ください。
http://www.es.osaka-u.ac.jp/access/
お問い合せ: 本ウェブサイトの「お問い合せ」のページをご参照ください。