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


蓮尾一郎 (東京大学大学院情報理工学系研究科)
  1. MMDSについて
  2. MMDSの教員・組織
  3. MMDSで学びたい方へ
  4. カリキュラム
  5. MMDSの活動

  6. 学内向け情報

大阪大学 数理・データ科学セミナー 数理モデルセミナーシリーズ第2回
超準解析による物理情報システムの形式検証―離散から連続・ ハイブリッドへ
Nonstandard Analysis and Formal Verification of Cyber-Physical Systems: From Discrete to Continuous and Hybrid Dynamics


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

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

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

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

講 師:
蓮尾一郎 (東京大学大学院情報理工学系研究科)
テーマ:
超準解析による物理情報システムの形式検証―離散から連続・ ハイブリッドへ
Nonstandard Analysis and Formal Verification of Cyber-Physical Systems: From Discrete to Continuous and Hybrid Dynamics
日 時:
2015年06月12日(金)16:45-17:45
場 所:
大阪大学 豊中キャンパス 基礎工国際棟シグマホール
参加費:
無料
アクセス:
会場までのアクセスは下記URLをご参照ください。
http://www.es.osaka-u.ac.jp/access/
お問い合せ:
本ウェブサイトの「お問い合せ」のページをご参照ください。