ERATO MMSDプロジェクト紹介
高信頼物理情報システムのための包括的研究

蓮尾 一郎
国立情報学研究所 (NII) システム設計数理国際研究センター センター長・准教授
JST ERATO 蓮尾メタ数理システムデザインプロジェクト 研究総括
総合研究大学院大学 准教授

アウトライン
ERATO MMSD プロジェクト概要
形式手法と物理情報システム
プロジェクトの研究開発状況
技術紹介
形式手法・テストによるシステム品質保証手法，特にサーチベーステスト
実行時監視
今後の協働に向けて
2

ERATO とは
国立研究開発法人 科学技術振興機構（JST）の，
戦略的創造研究推進事業プログラムの一つ
ERATO，CREST，さきがけ，ACT-I/ACT-X
規模の大きな研究費をもとに，既存の研究分野を超えた分野融合や新しいアプローチによって，挑戦的な基礎研究を推進
全ての学術分野から，毎年2-4件のプロジェクトを採択

3

Hasuo (NII, Tokyo)

ERATO MMSD 紹介
JST ERATO プロジェクト
2016/10-2022/03.
総勢50名規模の基礎研究プロジェクト
プロジェクト目標： 工業製品の設計サポート
形式手法の拡張．ソフトウェアから物理情報システムへ
安全性・信頼性，Veriﬁcation & Validation．「システムが期待通り動作するか」
特に自動運転を戦略的ターゲットに．U Waterloo と協働 www.autonomoose.net
研究体制
国際的体制．4つのグループの1つは @ U Waterloo．
雇用する研究員15名余のうち，外国人が半数以上
先端的・包括的学術研究を実システムに応用学際的 ”creative chaos” によるブレイクスルー
Waterloo・京大・阪大・九大のチームと協働しつつ，リソースの大部分を NII に集約
多様な背景： 論理学・代数学から形式手法，制御理論，機械学習，ソフトウェア工学まで
4
Hasuo (NII, Tokyo)

Our Organization
International and multi-disciplinary. “creative chaos”
Kyoto U IS Site:
Advanced Deductive
Verification
Leader:Kohei Suenaga
Kyoto U RIMS Site:
Categorical
Infrastructure
Leader:Masahito Hasegawa

Group 0 @ NII:
Metatheoretical Integration
Leader: Shin-ya Katsumata
Topics:Programming
Languages,
Formal Semantics,
Categorical Models,Mathematical
Logic, …

Group 3 @ NII:
Formal Methods andIntelligence
Leader: Fuyuki Ishikawa
Topics:SoftwareEngineering,Formal Modeling,
Testing, Safe &Explainable AI

Kyushu U Site:
Optimization for
CPS V&V
Leader:Hayato Waki

Group 2 @ U Waterloo:
Formal Methods in Industry
Leader: Krzysztof Czarnecki

Osaka U Site:
Control Theory for
CPS
Leader:Toshimitsu Ushio

Group 1 @ NII:
Heterogeneous Formal Methods
Leader: Ichiro Hasuo
Subleader: Masako Kishida
Topics:Automata Theory,
Control Theory,
Formal Verification,
Proof Assistants,
Automated
Deduction,
Runtime Verification

Topics:Automated
Driving, Software
Engineering,
Machine Learning

Hasuo (NII, Tokyo)

ERATO MMSD: プロジェクト目標
数理的技法を用いた工業製品設計の支援
形式手法の拡張：
ソフトウェアから物理情報システムへ
機械などの物理ダイナミクス（連続，アナログ）＋
計算機制御，ネットワーク（離散，デジタル）✓

theory of coalgebrasin K`(Be )Defn.

T (e) =

Thm.

A ::=
true methods| false | (suchA1 ^ A| ¬A | a1 < a2 |are valid in T (e)Coalgebraic
proof
as2 (bi)simulations)⇤⇤, where Be is a monad suited for e

Proof.

By the following characterizations in K`(Be ).

8x 2 N. A | 8x 2 R. A

FX
O
c
X

F behc /

F OZ
final
/Z

behc
system behavior

6

◆

FX
O
c
X

Ff
w

/ FY
O
d
/Y

f
simulation

今日の製造業における挑戦
複雑さの爆発http://www.popularmechanics.com/cars/how-to/
a7386/how-it-works-the-computer-inside-your-car/Clarus Concept of Operations. Publication No. FHWA-JPO-05-072, Federal Highway Administration (FHWA), 2005

新たな機能・応用
自動運転
wired.com

安全性保証と説明責任
オンデマンド生産,“Industrie 4.0”
7

automotiveit.eu

性能・機能が飛躍的に拡大，しかし工業製品の複雑さも飛躍的に拡大

製造業における困難
複雑さの爆発http://www.popularmechanics.com/cars/how-to/
a7386/how-it-works-the-computer-inside-your-car/

現代の工業製品におけるソフトウェア制御が原因

Clarus Concept of Operations. Publication No. FHWA-JPO-05-072, Federal Highway Administration (FHWA), 2005

新たな機能・応用
自動運転
ソフトウェアの品質向上手法を援用➜ 形式手法の活用
wired.com

安全性保証と説明責任
オンデマンド生産,“Industrie 4.0”
8

automotiveit.eu

アウトライン
ERATO MMSD プロジェクト概要
形式手法と物理情報システム
プロジェクトの研究開発状況
技術紹介
形式手法・テストによるシステム品質保証手法，特にサーチベーステスト
実行時監視
今後の協働に向けて
9

形式手法

formal methods（もともとは）ソフトウェアの
品質保証のための，数学的・記号論理的手法の総体
記号的であるため計算機実装が可能

計算機システムに対して多数の実績あり
IC design (Intel, …)* device drivers (Microsoft)* light-weight FM*(Facebook)

形式手法の例
形式検証 veriﬁcation
Input:a system model Ma specification 𝛗
Output: if M ⊨ 𝛗 or not
w/ a proof, if yes
w/ a counterexample,
if not* …

自動生成 synthesis
Input:
a specification 𝛗
Output: a system M
such that M ⊨ 𝛗or: a parameter ofa given (partial)
10
model

形式仕様記述speciﬁcation
Expressing aproperty desired ina formal language
machinerepresentablebasis for verif. &synthesis

形式検証の例１： 定理証明
例: Hoare 論理による定理証明
イメージ： 紙とペンで証明を書くのと同じ
しかし，人力だと間違えるので，計算機上で．
記号列で証明を表現 ➜ 各ステップの正当性をプログラム（証明支援系）がチェックできれば証明の自動探索（定理証明器）（原理上は）無限の入力空間をすべてカバーできる
証明では「i を入力の自然数とする」とかけますね
数学的証明という，強い品質保証

program

Theorem forall_exists : (forall P : Set->Prop,(forall x, ~(P x)) -> ~(exists x, P x)).
Proof.
intros P.
intros forall_x_not_Px.
unfold not.
intros exists_x_Px.
destruct exists_x_Px as [ witness proof_of_Pwitness].
pose (not_Pwitness := forall_x_not_Px witness).
unfold not in not_Pwitness.
pose (proof_of_False := not_Pwitness proof_of_Pwitness).
case proof_of_False.
Qed.

Proof
searchhoge

specificationk = N!
after
execution

proof
11

A Coq proof of ∀x. ¬P(x) → ¬ ∃x. P(x)ビジネスでの証明
はい，大丈夫です．
なぜなら，任意の状態 s に．．．（読んでる）
なるほど．それでは1
基いただこう．

対して，ゴンドラ g1 の位置
を x1 とすると，．．．

この駐車場，
どうでしょう．

ゴンドラが衝突したりしない？ 大丈夫？

形式検証の例２： モデル検査
オートマトンのアルゴリズムによる「自動証明」
主にグラフの到達可能性判定に帰着
オートマトンは有限 ➜ 数え上げによる自動証明が可能
例： 以下のオートマトンにて， 👿 に至ることはない (*)

b

a

（不正解）
仕様 (*) をすべての入力について確かめる（入力は無限個あるので無理）

b
a,b

👿

（正解）
到達可能な領域を計算し（グラaa, bフ探索，有限時間で飽和），👿
が含まれないことを確かめる
13

形式手法の歴史（超ダイジェスト）
ソフトウェアの大規模化
ネットワー
ク，分散並列物理システム1970頃 形式手法によるソフトウェア品質保証（ソフトウェア検証）の研究開始．定理証明，モデル検査
1990頃 ソフトウェア検証のツール化・実応用加速定理証明： Isabelle, Coq, PVS, …
モデル検査： SPIN, SMV/NuSMV, mCRL2, PRISM,
Uppaal, …

との融合

統計的機械学
習の能力向上2006 物理情報システム (Cyber-Physical Systems, CPS)への応用開始．ソフトウェア検証 ＋ 制御理論
（この経緯は [奥村，研究 技術 計画 2017] に詳しい）

2016 機械学習システムへの応用．
形式的推論と統計的推論
14

sha1_base64="hv19xxln5Ihgt0PDz00mX3beYGs=">AAACF3icbZC7TsMwFIadcivlVmCEwaJCKkuVICQYq8LAWBC9SE1UOY7TWnXsYDtAFXXhLXgDVngBNsTKyM6D4LYZoOVIln79/znH9ufHjCpt219WbmFxaXklv1pYW9/Y3Cpu7zSVSCQmDSyYkG0fKcIoJw1NNSPtWBIU+Yy0/MH5OG/dEamo4Dd6GBMvQj1OQ4qRNla3uO/WxEM5dq9pr6+RlOLevaAoEjyAt0fdYsmu2JOC88LJRAlkVe8Wv91A4CQiXGOGlOo4dqy9FElNMSOjgpsoEiM8QD3SMZKjiCgvnfxiBA+NE8BQSHO4hhP390SKIqWGkW86I6T7ajYbm/9lnUSHZ15KeZxowvH0ojBhUAs4RgIDKgnWbGgEwpKat0LcRxJhbcAV3PHCDGHqCxaMDBZnFsK8aB5XHLviXJ2UqrUMUB7sgQNQBg44BVVwCeqgATB4BM/gBbxaT9ab9W59TFtzVjazC/6U9fkDl7ugSA==</latexit>

sha1_base64="hv19xxln5Ihgt0PDz00mX3beYGs=">AAACF3icbZC7TsMwFIadcivlVmCEwaJCKkuVICQYq8LAWBC9SE1UOY7TWnXsYDtAFXXhLXgDVngBNsTKyM6D4LYZoOVIln79/znH9ufHjCpt219WbmFxaXklv1pYW9/Y3Cpu7zSVSCQmDSyYkG0fKcIoJw1NNSPtWBIU+Yy0/MH5OG/dEamo4Dd6GBMvQj1OQ4qRNla3uO/WxEM5dq9pr6+RlOLevaAoEjyAt0fdYsmu2JOC88LJRAlkVe8Wv91A4CQiXGOGlOo4dqy9FElNMSOjgpsoEiM8QD3SMZKjiCgvnfxiBA+NE8BQSHO4hhP390SKIqWGkW86I6T7ajYbm/9lnUSHZ15KeZxowvH0ojBhUAs4RgIDKgnWbGgEwpKat0LcRxJhbcAV3PHCDGHqCxaMDBZnFsK8aB5XHLviXJ2UqrUMUB7sgQNQBg44BVVwCeqgATB4BM/gBbxaT9ab9W59TFtzVjazC/6U9fkDl7ugSA==</latexit><latexit

sha1_base64="hv19xxln5Ihgt0PDz00mX3beYGs=">AAACF3icbZC7TsMwFIadcivlVmCEwaJCKkuVICQYq8LAWBC9SE1UOY7TWnXsYDtAFXXhLXgDVngBNsTKyM6D4LYZoOVIln79/znH9ufHjCpt219WbmFxaXklv1pYW9/Y3Cpu7zSVSCQmDSyYkG0fKcIoJw1NNSPtWBIU+Yy0/MH5OG/dEamo4Dd6GBMvQj1OQ4qRNla3uO/WxEM5dq9pr6+RlOLevaAoEjyAt0fdYsmu2JOC88LJRAlkVe8Wv91A4CQiXGOGlOo4dqy9FElNMSOjgpsoEiM8QD3SMZKjiCgvnfxiBA+NE8BQSHO4hhP390SKIqWGkW86I6T7ajYbm/9lnUSHZ15KeZxowvH0ojBhUAs4RgIDKgnWbGgEwpKat0LcRxJhbcAV3PHCDGHqCxaMDBZnFsK8aB5XHLviXJ2UqrUMUB7sgQNQBg44BVVwCeqgATB4BM/gBbxaT9ab9W59TFtzVjazC/6U9fkDl7ugSA==</latexit><latexit

sha1_base64="hv19xxln5Ihgt0PDz00mX3beYGs=">AAACF3icbZC7TsMwFIadcivlVmCEwaJCKkuVICQYq8LAWBC9SE1UOY7TWnXsYDtAFXXhLXgDVngBNsTKyM6D4LYZoOVIln79/znH9ufHjCpt219WbmFxaXklv1pYW9/Y3Cpu7zSVSCQmDSyYkG0fKcIoJw1NNSPtWBIU+Yy0/MH5OG/dEamo4Dd6GBMvQj1OQ4qRNla3uO/WxEM5dq9pr6+RlOLevaAoEjyAt0fdYsmu2JOC88LJRAlkVe8Wv91A4CQiXGOGlOo4dqy9FElNMSOjgpsoEiM8QD3SMZKjiCgvnfxiBA+NE8BQSHO4hhP390SKIqWGkW86I6T7ajYbm/9lnUSHZ15KeZxowvH0ojBhUAs4RgIDKgnWbGgEwpKat0LcRxJhbcAV3PHCDGHqCxaMDBZnFsK8aB5XHLviXJ2UqrUMUB7sgQNQBg44BVVwCeqgATB4BM/gBbxaT9ab9W59TFtzVjazC/6U9fkDl7ugSA==</latexit><latexit⇤(p ) ⌃q)<latexit

15

sha1_base64="OLHwdpyatx3yKIFqo/K47yv4v90=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDIjgm6EohuXFexD2qFk0kwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy09cCFwzn3JveeIGJUG9f9cnJLyyura/n1wsbm1vZOcXevoWWsMKljyaRqBUgTRgWpG2oYaUWKIB4w0gyGN6nffCRKUynuzTgiPkd9QUOKkbHSw+j4KiyPTuOTbrHkVtwp4CLxMlICGWrd4nenJ3HMiTCYIa3bnhsZP0HKUMzIpNCJNYkQHqI+aVsqECfaT6YLT+CRVXowlMqWMHCq/p5IENd6zAPbyZEZ6HkvFf/z2rEJL/2Eiig2RODZR2HMoJEwvR72qCLYsLElCCtqd4V4gBTCxmZU6KQPZmklgWS9iY3Fmw9hkTTOKp5b8e7OS9XrLKA8OACHoAw8cAGq4BbUQB1gwMEzeAGvzpPz5rw7H7PWnJPN7IM/cD5/AH9Ul5E=</latexit>

sha1_base64="OLHwdpyatx3yKIFqo/K47yv4v90=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDIjgm6EohuXFexD2qFk0kwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy09cCFwzn3JveeIGJUG9f9cnJLyyura/n1wsbm1vZOcXevoWWsMKljyaRqBUgTRgWpG2oYaUWKIB4w0gyGN6nffCRKUynuzTgiPkd9QUOKkbHSw+j4KiyPTuOTbrHkVtwp4CLxMlICGWrd4nenJ3HMiTCYIa3bnhsZP0HKUMzIpNCJNYkQHqI+aVsqECfaT6YLT+CRVXowlMqWMHCq/p5IENd6zAPbyZEZ6HkvFf/z2rEJL/2Eiig2RODZR2HMoJEwvR72qCLYsLElCCtqd4V4gBTCxmZU6KQPZmklgWS9iY3Fmw9hkTTOKp5b8e7OS9XrLKA8OACHoAw8cAGq4BbUQB1gwMEzeAGvzpPz5rw7H7PWnJPN7IM/cD5/AH9Ul5E=</latexit><latexit

sha1_base64="OLHwdpyatx3yKIFqo/K47yv4v90=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDIjgm6EohuXFexD2qFk0kwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy09cCFwzn3JveeIGJUG9f9cnJLyyura/n1wsbm1vZOcXevoWWsMKljyaRqBUgTRgWpG2oYaUWKIB4w0gyGN6nffCRKUynuzTgiPkd9QUOKkbHSw+j4KiyPTuOTbrHkVtwp4CLxMlICGWrd4nenJ3HMiTCYIa3bnhsZP0HKUMzIpNCJNYkQHqI+aVsqECfaT6YLT+CRVXowlMqWMHCq/p5IENd6zAPbyZEZ6HkvFf/z2rEJL/2Eiig2RODZR2HMoJEwvR72qCLYsLElCCtqd4V4gBTCxmZU6KQPZmklgWS9iY3Fmw9hkTTOKp5b8e7OS9XrLKA8OACHoAw8cAGq4BbUQB1gwMEzeAGvzpPz5rw7H7PWnJPN7IM/cD5/AH9Ul5E=</latexit><latexit

sha1_base64="OLHwdpyatx3yKIFqo/K47yv4v90=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDIjgm6EohuXFexD2qFk0kwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy09cCFwzn3JveeIGJUG9f9cnJLyyura/n1wsbm1vZOcXevoWWsMKljyaRqBUgTRgWpG2oYaUWKIB4w0gyGN6nffCRKUynuzTgiPkd9QUOKkbHSw+j4KiyPTuOTbrHkVtwp4CLxMlICGWrd4nenJ3HMiTCYIa3bnhsZP0HKUMzIpNCJNYkQHqI+aVsqECfaT6YLT+CRVXowlMqWMHCq/p5IENd6zAPbyZEZ6HkvFf/z2rEJL/2Eiig2RODZR2HMoJEwvR72qCLYsLElCCtqd4V4gBTCxmZU6KQPZmklgWS9iY3Fmw9hkTTOKp5b8e7OS9XrLKA8OACHoAw8cAGq4BbUQB1gwMEzeAGvzpPz5rw7H7PWnJPN7IM/cD5/AH9Ul5E=</latexit><latexit

sha1_base64="OLHwdpyatx3yKIFqo/K47yv4v90=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDIjgm6EohuXFexD2qFk0kwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy09cCFwzn3JveeIGJUG9f9cnJLyyura/n1wsbm1vZOcXevoWWsMKljyaRqBUgTRgWpG2oYaUWKIB4w0gyGN6nffCRKUynuzTgiPkd9QUOKkbHSw+j4KiyPTuOTbrHkVtwp4CLxMlICGWrd4nenJ3HMiTCYIa3bnhsZP0HKUMzIpNCJNYkQHqI+aVsqECfaT6YLT+CRVXowlMqWMHCq/p5IENd6zAPbyZEZ6HkvFf/z2rEJL/2Eiig2RODZR2HMoJEwvR72qCLYsLElCCtqd4V4gBTCxmZU6KQPZmklgWS9iY3Fmw9hkTTOKp5b8e7OS9XrLKA8OACHoAw8cAGq4BbUQB1gwMEzeAGvzpPz5rw7H7PWnJPN7IM/cD5/AH9Ul5E=</latexit><latexit

sha1_base64="OLHwdpyatx3yKIFqo/K47yv4v90=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDIjgm6EohuXFexD2qFk0kwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy09cCFwzn3JveeIGJUG9f9cnJLyyura/n1wsbm1vZOcXevoWWsMKljyaRqBUgTRgWpG2oYaUWKIB4w0gyGN6nffCRKUynuzTgiPkd9QUOKkbHSw+j4KiyPTuOTbrHkVtwp4CLxMlICGWrd4nenJ3HMiTCYIa3bnhsZP0HKUMzIpNCJNYkQHqI+aVsqECfaT6YLT+CRVXowlMqWMHCq/p5IENd6zAPbyZEZ6HkvFf/z2rEJL/2Eiig2RODZR2HMoJEwvR72qCLYsLElCCtqd4V4gBTCxmZU6KQPZmklgWS9iY3Fmw9hkTTOKp5b8e7OS9XrLKA8OACHoAw8cAGq4BbUQB1gwMEzeAGvzpPz5rw7H7PWnJPN7IM/cD5/AH9Ul5E=</latexit><latexit

sha1_base64="Hx+nB8T5F5UCLoxoqCIXEBH+afA=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDLjRjdC0Y3LCvYh7VAymUwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy0euDC4Zx7k3tPEDOqjet+OoWl5ZXVteJ6aWNza3unvLvX0jJRmDSxZFJ1AqQJo4I0DTWMdGJFEA8YaQej68xvPxClqRR3ZhITn6OBoBHFyFjpfnx8GVXHp8lJv1xxa+4M8C/xclIBORr98lcvlDjhRBjMkNZdz42NnyJlKGZkWuolmsQIj9CAdC0ViBPtp7OFp/DIKiGMpLIlDJypPydSxLWe8MB2cmSGetHLxP+8bmKiCz+lIk4MEXj+UZQwaCTMrochVQQbNrEEYUXtrhAPkULY2IxKvezBPK00kCyc2li8xRD+ktZZzXNr3q1bqV/lARXBATgEVeCBc1AHN6ABmgADDp7AM3hxHp1X5815n7cWnHxmH/yC8/ENfhSXjQ==</latexit><latexit

sha1_base64="wdgUGz0/4fuZ88hKGlj8zgUTtXk=">AAAB93icbZDLSgMxGIX/qbdaq1a3boJFrCBlxo1uBMGNywr2Iu1QMmmmDU0yQ5KRlqE738CtvoA78Wnc+yBm2llo64HA4Zxc/nxBzJk2rvvlFNbWNza3itulnfLu3n7loNzSUaIIbZKIR6oTYE05k7RpmOG0EyuKRcBpOxjfZn37iSrNIvlgpjH1BR5KFjKCjY0eJ6fXYW1ynpz1K1W37s6FVo2XmyrkavQr371BRBJBpSEca9313Nj4KVaGEU5npV6iaYzJGA9p11qJBdV+Oh94hk5sMkBhpOySBs3T3ydSLLSeisDuFNiM9HKXhf913cSEV37KZJwYKsnioTDhyEQo+z0aMEWJ4VNrMFHMzorICCtMjGVU6mUX5rTSIOKDmcXiLUNYNa2LuufWvXsXinAEx1ADDy7hBu6gAU0gIOAFXuHNeXbenY8FwIKTkzyEP3I+fwD4XJYk</latexit><latexit

sha1_base64="wdgUGz0/4fuZ88hKGlj8zgUTtXk=">AAAB93icbZDLSgMxGIX/qbdaq1a3boJFrCBlxo1uBMGNywr2Iu1QMmmmDU0yQ5KRlqE738CtvoA78Wnc+yBm2llo64HA4Zxc/nxBzJk2rvvlFNbWNza3itulnfLu3n7loNzSUaIIbZKIR6oTYE05k7RpmOG0EyuKRcBpOxjfZn37iSrNIvlgpjH1BR5KFjKCjY0eJ6fXYW1ynpz1K1W37s6FVo2XmyrkavQr371BRBJBpSEca9313Nj4KVaGEU5npV6iaYzJGA9p11qJBdV+Oh94hk5sMkBhpOySBs3T3ydSLLSeisDuFNiM9HKXhf913cSEV37KZJwYKsnioTDhyEQo+z0aMEWJ4VNrMFHMzorICCtMjGVU6mUX5rTSIOKDmcXiLUNYNa2LuufWvXsXinAEx1ADDy7hBu6gAU0gIOAFXuHNeXbenY8FwIKTkzyEP3I+fwD4XJYk</latexit><latexit

sha1_base64="4LCzMseb0W4aHc9jzDSRRbHgPjA=">AAAB63icbZC7TsMwGIX/lFsJBcrMYlEhMVUJC4xILIxFoheprSrHcVqrjh3Zf5BK1Bdg5QXYEI/EzoPgtBmg5UiWjs7x5fcXZVJYDIIvr7azu7d/UD/0jxr+8clps9GzOjeMd5mW2gwiarkUindRoOSDzHCaRpL3o/l92fefubFCqydcZHyc0qkSiWAUXdSZNFtBO1iJbJuwMi2oNGl+j2LN8pQrZJJaOwyDDMcFNSiY5Et/lFueUTanUz50VtGU23GxGnNJLl0Sk0QbtxSSVfr7REFTaxdp5HamFGd2syvD/7phjsntuBAqy5Ertn4oySVBTco/k1gYzlAunKHMCDcrYTNqKENHxh+VF1aMikjLeOmohJsMtk3vuh0G7fAxgDqcwwVcQQg3cAcP0IEuMIjhFd68F+/d+1jTq3kVxjP4I+/zB6n+kjc=</latexit><latexit

sha1_base64="OLHwdpyatx3yKIFqo/K47yv4v90=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDIjgm6EohuXFexD2qFk0kwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy09cCFwzn3JveeIGJUG9f9cnJLyyura/n1wsbm1vZOcXevoWWsMKljyaRqBUgTRgWpG2oYaUWKIB4w0gyGN6nffCRKUynuzTgiPkd9QUOKkbHSw+j4KiyPTuOTbrHkVtwp4CLxMlICGWrd4nenJ3HMiTCYIa3bnhsZP0HKUMzIpNCJNYkQHqI+aVsqECfaT6YLT+CRVXowlMqWMHCq/p5IENd6zAPbyZEZ6HkvFf/z2rEJL/2Eiig2RODZR2HMoJEwvR72qCLYsLElCCtqd4V4gBTCxmZU6KQPZmklgWS9iY3Fmw9hkTTOKp5b8e7OS9XrLKA8OACHoAw8cAGq4BbUQB1gwMEzeAGvzpPz5rw7H7PWnJPN7IM/cD5/AH9Ul5E=</latexit><latexit

協働sha1_base64="OLHwdpyatx3yKIFqo/K47yv4v90=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDIjgm6EohuXFexD2qFk0kwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy09cCFwzn3JveeIGJUG9f9cnJLyyura/n1wsbm1vZOcXevoWWsMKljyaRqBUgTRgWpG2oYaUWKIB4w0gyGN6nffCRKUynuzTgiPkd9QUOKkbHSw+j4KiyPTuOTbrHkVtwp4CLxMlICGWrd4nenJ3HMiTCYIa3bnhsZP0HKUMzIpNCJNYkQHqI+aVsqECfaT6YLT+CRVXowlMqWMHCq/p5IENd6zAPbyZEZ6HkvFf/z2rEJL/2Eiig2RODZR2HMoJEwvR72qCLYsLElCCtqd4V4gBTCxmZU6KQPZmklgWS9iY3Fmw9hkTTOKp5b8e7OS9XrLKA8OACHoAw8cAGq4BbUQB1gwMEzeAGvzpPz5rw7H7PWnJPN7IM/cD5/AH9Ul5E=</latexit><latexit

制御理論
sha1_base64="OLHwdpyatx3yKIFqo/K47yv4v90=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDIjgm6EohuXFexD2qFk0kwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy09cCFwzn3JveeIGJUG9f9cnJLyyura/n1wsbm1vZOcXevoWWsMKljyaRqBUgTRgWpG2oYaUWKIB4w0gyGN6nffCRKUynuzTgiPkd9QUOKkbHSw+j4KiyPTuOTbrHkVtwp4CLxMlICGWrd4nenJ3HMiTCYIa3bnhsZP0HKUMzIpNCJNYkQHqI+aVsqECfaT6YLT+CRVXowlMqWMHCq/p5IENd6zAPbyZEZ6HkvFf/z2rEJL/2Eiig2RODZR2HMoJEwvR72qCLYsLElCCtqd4V4gBTCxmZU6KQPZmklgWS9iY3Fmw9hkTTOKp5b8e7OS9XrLKA8OACHoAw8cAGq4BbUQB1gwMEzeAGvzpPz5rw7H7PWnJPN7IM/cD5/AH9Ul5E=</latexit><latexit

形式手法<latexit

これまでの物理情報システム研究（特に安全性・信頼性の側面）
物理情報システム（特に hybrid system）
解析
x0 = f (x, u)

追いつかなければ…??

物理情報システム研究への取り組みでは欧米が先行
米国： NSF の CPS 研究イニシアチブ (2006-)

欧州： 形式手法の定量的拡張（確率，時間，…）

sha1_base64="hv19xxln5Ihgt0PDz00mX3beYGs=">AAACF3icbZC7TsMwFIadcivlVmCEwaJCKkuVICQYq8LAWBC9SE1UOY7TWnXsYDtAFXXhLXgDVngBNsTKyM6D4LYZoOVIln79/znH9ufHjCpt219WbmFxaXklv1pYW9/Y3Cpu7zSVSCQmDSyYkG0fKcIoJw1NNSPtWBIU+Yy0/MH5OG/dEamo4Dd6GBMvQj1OQ4qRNla3uO/WxEM5dq9pr6+RlOLevaAoEjyAt0fdYsmu2JOC88LJRAlkVe8Wv91A4CQiXGOGlOo4dqy9FElNMSOjgpsoEiM8QD3SMZKjiCgvnfxiBA+NE8BQSHO4hhP390SKIqWGkW86I6T7ajYbm/9lnUSHZ15KeZxowvH0ojBhUAs4RgIDKgnWbGgEwpKat0LcRxJhbcAV3PHCDGHqCxaMDBZnFsK8aB5XHLviXJ2UqrUMUB7sgQNQBg44BVVwCeqgATB4BM/gBbxaT9ab9W59TFtzVjazC/6U9fkDl7ugSA==</latexit>

sha1_base64="hv19xxln5Ihgt0PDz00mX3beYGs=">AAACF3icbZC7TsMwFIadcivlVmCEwaJCKkuVICQYq8LAWBC9SE1UOY7TWnXsYDtAFXXhLXgDVngBNsTKyM6D4LYZoOVIln79/znH9ufHjCpt219WbmFxaXklv1pYW9/Y3Cpu7zSVSCQmDSyYkG0fKcIoJw1NNSPtWBIU+Yy0/MH5OG/dEamo4Dd6GBMvQj1OQ4qRNla3uO/WxEM5dq9pr6+RlOLevaAoEjyAt0fdYsmu2JOC88LJRAlkVe8Wv91A4CQiXGOGlOo4dqy9FElNMSOjgpsoEiM8QD3SMZKjiCgvnfxiBA+NE8BQSHO4hhP390SKIqWGkW86I6T7ajYbm/9lnUSHZ15KeZxowvH0ojBhUAs4RgIDKgnWbGgEwpKat0LcRxJhbcAV3PHCDGHqCxaMDBZnFsK8aB5XHLviXJ2UqrUMUB7sgQNQBg44BVVwCeqgATB4BM/gBbxaT9ab9W59TFtzVjazC/6U9fkDl7ugSA==</latexit><latexit

sha1_base64="hv19xxln5Ihgt0PDz00mX3beYGs=">AAACF3icbZC7TsMwFIadcivlVmCEwaJCKkuVICQYq8LAWBC9SE1UOY7TWnXsYDtAFXXhLXgDVngBNsTKyM6D4LYZoOVIln79/znH9ufHjCpt219WbmFxaXklv1pYW9/Y3Cpu7zSVSCQmDSyYkG0fKcIoJw1NNSPtWBIU+Yy0/MH5OG/dEamo4Dd6GBMvQj1OQ4qRNla3uO/WxEM5dq9pr6+RlOLevaAoEjyAt0fdYsmu2JOC88LJRAlkVe8Wv91A4CQiXGOGlOo4dqy9FElNMSOjgpsoEiM8QD3SMZKjiCgvnfxiBA+NE8BQSHO4hhP390SKIqWGkW86I6T7ajYbm/9lnUSHZ15KeZxowvH0ojBhUAs4RgIDKgnWbGgEwpKat0LcRxJhbcAV3PHCDGHqCxaMDBZnFsK8aB5XHLviXJ2UqrUMUB7sgQNQBg44BVVwCeqgATB4BM/gBbxaT9ab9W59TFtzVjazC/6U9fkDl7ugSA==</latexit><latexit

sha1_base64="hv19xxln5Ihgt0PDz00mX3beYGs=">AAACF3icbZC7TsMwFIadcivlVmCEwaJCKkuVICQYq8LAWBC9SE1UOY7TWnXsYDtAFXXhLXgDVngBNsTKyM6D4LYZoOVIln79/znH9ufHjCpt219WbmFxaXklv1pYW9/Y3Cpu7zSVSCQmDSyYkG0fKcIoJw1NNSPtWBIU+Yy0/MH5OG/dEamo4Dd6GBMvQj1OQ4qRNla3uO/WxEM5dq9pr6+RlOLevaAoEjyAt0fdYsmu2JOC88LJRAlkVe8Wv91A4CQiXGOGlOo4dqy9FElNMSOjgpsoEiM8QD3SMZKjiCgvnfxiBA+NE8BQSHO4hhP390SKIqWGkW86I6T7ajYbm/9lnUSHZ15KeZxowvH0ojBhUAs4RgIDKgnWbGgEwpKat0LcRxJhbcAV3PHCDGHqCxaMDBZnFsK8aB5XHLviXJ2UqrUMUB7sgQNQBg44BVVwCeqgATB4BM/gBbxaT9ab9W59TFtzVjazC/6U9fkDl7ugSA==</latexit><latexit⇤(p ) ⌃q)<latexit

ホワイトボックスモデルの完全な理解が前提

16

sha1_base64="OLHwdpyatx3yKIFqo/K47yv4v90=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDIjgm6EohuXFexD2qFk0kwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy09cCFwzn3JveeIGJUG9f9cnJLyyura/n1wsbm1vZOcXevoWWsMKljyaRqBUgTRgWpG2oYaUWKIB4w0gyGN6nffCRKUynuzTgiPkd9QUOKkbHSw+j4KiyPTuOTbrHkVtwp4CLxMlICGWrd4nenJ3HMiTCYIa3bnhsZP0HKUMzIpNCJNYkQHqI+aVsqECfaT6YLT+CRVXowlMqWMHCq/p5IENd6zAPbyZEZ6HkvFf/z2rEJL/2Eiig2RODZR2HMoJEwvR72qCLYsLElCCtqd4V4gBTCxmZU6KQPZmklgWS9iY3Fmw9hkTTOKp5b8e7OS9XrLKA8OACHoAw8cAGq4BbUQB1gwMEzeAGvzpPz5rw7H7PWnJPN7IM/cD5/AH9Ul5E=</latexit>

sha1_base64="OLHwdpyatx3yKIFqo/K47yv4v90=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDIjgm6EohuXFexD2qFk0kwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy09cCFwzn3JveeIGJUG9f9cnJLyyura/n1wsbm1vZOcXevoWWsMKljyaRqBUgTRgWpG2oYaUWKIB4w0gyGN6nffCRKUynuzTgiPkd9QUOKkbHSw+j4KiyPTuOTbrHkVtwp4CLxMlICGWrd4nenJ3HMiTCYIa3bnhsZP0HKUMzIpNCJNYkQHqI+aVsqECfaT6YLT+CRVXowlMqWMHCq/p5IENd6zAPbyZEZ6HkvFf/z2rEJL/2Eiig2RODZR2HMoJEwvR72qCLYsLElCCtqd4V4gBTCxmZU6KQPZmklgWS9iY3Fmw9hkTTOKp5b8e7OS9XrLKA8OACHoAw8cAGq4BbUQB1gwMEzeAGvzpPz5rw7H7PWnJPN7IM/cD5/AH9Ul5E=</latexit><latexit

sha1_base64="OLHwdpyatx3yKIFqo/K47yv4v90=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDIjgm6EohuXFexD2qFk0kwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy09cCFwzn3JveeIGJUG9f9cnJLyyura/n1wsbm1vZOcXevoWWsMKljyaRqBUgTRgWpG2oYaUWKIB4w0gyGN6nffCRKUynuzTgiPkd9QUOKkbHSw+j4KiyPTuOTbrHkVtwp4CLxMlICGWrd4nenJ3HMiTCYIa3bnhsZP0HKUMzIpNCJNYkQHqI+aVsqECfaT6YLT+CRVXowlMqWMHCq/p5IENd6zAPbyZEZ6HkvFf/z2rEJL/2Eiig2RODZR2HMoJEwvR72qCLYsLElCCtqd4V4gBTCxmZU6KQPZmklgWS9iY3Fmw9hkTTOKp5b8e7OS9XrLKA8OACHoAw8cAGq4BbUQB1gwMEzeAGvzpPz5rw7H7PWnJPN7IM/cD5/AH9Ul5E=</latexit><latexit

sha1_base64="OLHwdpyatx3yKIFqo/K47yv4v90=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDIjgm6EohuXFexD2qFk0kwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy09cCFwzn3JveeIGJUG9f9cnJLyyura/n1wsbm1vZOcXevoWWsMKljyaRqBUgTRgWpG2oYaUWKIB4w0gyGN6nffCRKUynuzTgiPkd9QUOKkbHSw+j4KiyPTuOTbrHkVtwp4CLxMlICGWrd4nenJ3HMiTCYIa3bnhsZP0HKUMzIpNCJNYkQHqI+aVsqECfaT6YLT+CRVXowlMqWMHCq/p5IENd6zAPbyZEZ6HkvFf/z2rEJL/2Eiig2RODZR2HMoJEwvR72qCLYsLElCCtqd4V4gBTCxmZU6KQPZmklgWS9iY3Fmw9hkTTOKp5b8e7OS9XrLKA8OACHoAw8cAGq4BbUQB1gwMEzeAGvzpPz5rw7H7PWnJPN7IM/cD5/AH9Ul5E=</latexit><latexit

sha1_base64="OLHwdpyatx3yKIFqo/K47yv4v90=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDIjgm6EohuXFexD2qFk0kwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy09cCFwzn3JveeIGJUG9f9cnJLyyura/n1wsbm1vZOcXevoWWsMKljyaRqBUgTRgWpG2oYaUWKIB4w0gyGN6nffCRKUynuzTgiPkd9QUOKkbHSw+j4KiyPTuOTbrHkVtwp4CLxMlICGWrd4nenJ3HMiTCYIa3bnhsZP0HKUMzIpNCJNYkQHqI+aVsqECfaT6YLT+CRVXowlMqWMHCq/p5IENd6zAPbyZEZ6HkvFf/z2rEJL/2Eiig2RODZR2HMoJEwvR72qCLYsLElCCtqd4V4gBTCxmZU6KQPZmklgWS9iY3Fmw9hkTTOKp5b8e7OS9XrLKA8OACHoAw8cAGq4BbUQB1gwMEzeAGvzpPz5rw7H7PWnJPN7IM/cD5/AH9Ul5E=</latexit><latexit

sha1_base64="OLHwdpyatx3yKIFqo/K47yv4v90=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDIjgm6EohuXFexD2qFk0kwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy09cCFwzn3JveeIGJUG9f9cnJLyyura/n1wsbm1vZOcXevoWWsMKljyaRqBUgTRgWpG2oYaUWKIB4w0gyGN6nffCRKUynuzTgiPkd9QUOKkbHSw+j4KiyPTuOTbrHkVtwp4CLxMlICGWrd4nenJ3HMiTCYIa3bnhsZP0HKUMzIpNCJNYkQHqI+aVsqECfaT6YLT+CRVXowlMqWMHCq/p5IENd6zAPbyZEZ6HkvFf/z2rEJL/2Eiig2RODZR2HMoJEwvR72qCLYsLElCCtqd4V4gBTCxmZU6KQPZmklgWS9iY3Fmw9hkTTOKp5b8e7OS9XrLKA8OACHoAw8cAGq4BbUQB1gwMEzeAGvzpPz5rw7H7PWnJPN7IM/cD5/AH9Ul5E=</latexit><latexit

sha1_base64="Hx+nB8T5F5UCLoxoqCIXEBH+afA=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDLjRjdC0Y3LCvYh7VAymUwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy0euDC4Zx7k3tPEDOqjet+OoWl5ZXVteJ6aWNza3unvLvX0jJRmDSxZFJ1AqQJo4I0DTWMdGJFEA8YaQej68xvPxClqRR3ZhITn6OBoBHFyFjpfnx8GVXHp8lJv1xxa+4M8C/xclIBORr98lcvlDjhRBjMkNZdz42NnyJlKGZkWuolmsQIj9CAdC0ViBPtp7OFp/DIKiGMpLIlDJypPydSxLWe8MB2cmSGetHLxP+8bmKiCz+lIk4MEXj+UZQwaCTMrochVQQbNrEEYUXtrhAPkULY2IxKvezBPK00kCyc2li8xRD+ktZZzXNr3q1bqV/lARXBATgEVeCBc1AHN6ABmgADDp7AM3hxHp1X5815n7cWnHxmH/yC8/ENfhSXjQ==</latexit><latexit

sha1_base64="wdgUGz0/4fuZ88hKGlj8zgUTtXk=">AAAB93icbZDLSgMxGIX/qbdaq1a3boJFrCBlxo1uBMGNywr2Iu1QMmmmDU0yQ5KRlqE738CtvoA78Wnc+yBm2llo64HA4Zxc/nxBzJk2rvvlFNbWNza3itulnfLu3n7loNzSUaIIbZKIR6oTYE05k7RpmOG0EyuKRcBpOxjfZn37iSrNIvlgpjH1BR5KFjKCjY0eJ6fXYW1ynpz1K1W37s6FVo2XmyrkavQr371BRBJBpSEca9313Nj4KVaGEU5npV6iaYzJGA9p11qJBdV+Oh94hk5sMkBhpOySBs3T3ydSLLSeisDuFNiM9HKXhf913cSEV37KZJwYKsnioTDhyEQo+z0aMEWJ4VNrMFHMzorICCtMjGVU6mUX5rTSIOKDmcXiLUNYNa2LuufWvXsXinAEx1ADDy7hBu6gAU0gIOAFXuHNeXbenY8FwIKTkzyEP3I+fwD4XJYk</latexit><latexit

sha1_base64="wdgUGz0/4fuZ88hKGlj8zgUTtXk=">AAAB93icbZDLSgMxGIX/qbdaq1a3boJFrCBlxo1uBMGNywr2Iu1QMmmmDU0yQ5KRlqE738CtvoA78Wnc+yBm2llo64HA4Zxc/nxBzJk2rvvlFNbWNza3itulnfLu3n7loNzSUaIIbZKIR6oTYE05k7RpmOG0EyuKRcBpOxjfZn37iSrNIvlgpjH1BR5KFjKCjY0eJ6fXYW1ynpz1K1W37s6FVo2XmyrkavQr371BRBJBpSEca9313Nj4KVaGEU5npV6iaYzJGA9p11qJBdV+Oh94hk5sMkBhpOySBs3T3ydSLLSeisDuFNiM9HKXhf913cSEV37KZJwYKsnioTDhyEQo+z0aMEWJ4VNrMFHMzorICCtMjGVU6mUX5rTSIOKDmcXiLUNYNa2LuufWvXsXinAEx1ADDy7hBu6gAU0gIOAFXuHNeXbenY8FwIKTkzyEP3I+fwD4XJYk</latexit><latexit

sha1_base64="4LCzMseb0W4aHc9jzDSRRbHgPjA=">AAAB63icbZC7TsMwGIX/lFsJBcrMYlEhMVUJC4xILIxFoheprSrHcVqrjh3Zf5BK1Bdg5QXYEI/EzoPgtBmg5UiWjs7x5fcXZVJYDIIvr7azu7d/UD/0jxr+8clps9GzOjeMd5mW2gwiarkUindRoOSDzHCaRpL3o/l92fefubFCqydcZHyc0qkSiWAUXdSZNFtBO1iJbJuwMi2oNGl+j2LN8pQrZJJaOwyDDMcFNSiY5Et/lFueUTanUz50VtGU23GxGnNJLl0Sk0QbtxSSVfr7REFTaxdp5HamFGd2syvD/7phjsntuBAqy5Ertn4oySVBTco/k1gYzlAunKHMCDcrYTNqKENHxh+VF1aMikjLeOmohJsMtk3vuh0G7fAxgDqcwwVcQQg3cAcP0IEuMIjhFd68F+/d+1jTq3kVxjP4I+/zB6n+kjc=</latexit><latexit

sha1_base64="OLHwdpyatx3yKIFqo/K47yv4v90=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDIjgm6EohuXFexD2qFk0kwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy09cCFwzn3JveeIGJUG9f9cnJLyyura/n1wsbm1vZOcXevoWWsMKljyaRqBUgTRgWpG2oYaUWKIB4w0gyGN6nffCRKUynuzTgiPkd9QUOKkbHSw+j4KiyPTuOTbrHkVtwp4CLxMlICGWrd4nenJ3HMiTCYIa3bnhsZP0HKUMzIpNCJNYkQHqI+aVsqECfaT6YLT+CRVXowlMqWMHCq/p5IENd6zAPbyZEZ6HkvFf/z2rEJL/2Eiig2RODZR2HMoJEwvR72qCLYsLElCCtqd4V4gBTCxmZU6KQPZmklgWS9iY3Fmw9hkTTOKp5b8e7OS9XrLKA8OACHoAw8cAGq4BbUQB1gwMEzeAGvzpPz5rw7H7PWnJPN7IM/cD5/AH9Ul5E=</latexit><latexit

sha1_base64="OLHwdpyatx3yKIFqo/K47yv4v90=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDIjgm6EohuXFexD2qFk0kwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy09cCFwzn3JveeIGJUG9f9cnJLyyura/n1wsbm1vZOcXevoWWsMKljyaRqBUgTRgWpG2oYaUWKIB4w0gyGN6nffCRKUynuzTgiPkd9QUOKkbHSw+j4KiyPTuOTbrHkVtwp4CLxMlICGWrd4nenJ3HMiTCYIa3bnhsZP0HKUMzIpNCJNYkQHqI+aVsqECfaT6YLT+CRVXowlMqWMHCq/p5IENd6zAPbyZEZ6HkvFf/z2rEJL/2Eiig2RODZR2HMoJEwvR72qCLYsLElCCtqd4V4gBTCxmZU6KQPZmklgWS9iY3Fmw9hkTTOKp5b8e7OS9XrLKA8OACHoAw8cAGq4BbUQB1gwMEzeAGvzpPz5rw7H7PWnJPN7IM/cD5/AH9Ul5E=</latexit><latexit

協働sha1_base64="OLHwdpyatx3yKIFqo/K47yv4v90=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDIjgm6EohuXFexD2qFk0kwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy09cCFwzn3JveeIGJUG9f9cnJLyyura/n1wsbm1vZOcXevoWWsMKljyaRqBUgTRgWpG2oYaUWKIB4w0gyGN6nffCRKUynuzTgiPkd9QUOKkbHSw+j4KiyPTuOTbrHkVtwp4CLxMlICGWrd4nenJ3HMiTCYIa3bnhsZP0HKUMzIpNCJNYkQHqI+aVsqECfaT6YLT+CRVXowlMqWMHCq/p5IENd6zAPbyZEZ6HkvFf/z2rEJL/2Eiig2RODZR2HMoJEwvR72qCLYsLElCCtqd4V4gBTCxmZU6KQPZmklgWS9iY3Fmw9hkTTOKp5b8e7OS9XrLKA8OACHoAw8cAGq4BbUQB1gwMEzeAGvzpPz5rw7H7PWnJPN7IM/cD5/AH9Ul5E=</latexit><latexit

形式手法<latexit

これまでの物理情報システム研究（特に安全性・信頼性の側面）
物理情報システム（特に hybrid system）
解析

制御理論
x0 = f (x, u)

課題： 実システムに対するスケーラビリティ

可能？
役に立つ？

結論の数学的正しさを絶対視

不確かさを許容する余地が少ない ➜ 統計的機械学習との相性の問題

ERATO MMSD の研究開発の目標：
これらの柔軟なミックス ➜ 実システムへ応用

ソフトウェア品質保証におけるスペクトル
形式手法

テスト test

自動定理証明

モデル検査
低

コスト

ブラックボックス

対話定理証明高

ホワイトボックスモデルを要求

モデルを許容高自動化の度合い低自動

経験論的保証専門家を月・年単位で拘束低保証の網羅性

高低保証の数学的厳密性

高数学的保証 ➜ 「形式検証」
17

スケールダウンできる形式手法
ご利益

ご利益

✔
コスト

✘
コスト

形式手法の多くはスケールダウンできない
ホワイトボックスモデルを要求．
全てのコンポーネントの形式モデル
ホワイトボックスモデルがないと何もできない ➜ ご利益 0「まずホワイトボックスモデルを書いてください．話はそれからだ」
ERATO MMSD の目指すところ
テストも組み合わせた，柔軟なソリューションを提案
応用シナリオ・リソースに合わせた品質保証
18アウトライン
ERATO MMSD プロジェクト概要
形式手法と物理情報システム
プロジェクトの研究開発状況
技術紹介
形式手法・テストによるシステム品質保証手法，特にサーチベーステスト
実行時監視
今後の協働に向けて
19物理情報システムのための
分野横断： ERATO MMSDの場合
応用

F

物理情報システムの品質保証（特に自動車）

機械学習・AI

ソフトウェア科学
形式手法

D

B
E

制御理論

C

ソフトウェア工学

A

基礎

（メタ）
数理的基盤
20

研究体制

Group 2
物理情報システムの品質保証（特に自動車）F

G0： メタ理論的統合グループ（勝股）
論理学，代数学，圏論，プログラミング言語理論，…
G1： ヘテロジニアス
ソフトウェア科学
形式手法グループ（蓮尾・岸田）
形式手法
ソフトウェア科学，
B
制御理論，形式手法，モデル検査，
自動定理証明，…
制御理論
G2： 産業応用グループ(Czarnecki)
自動運転システム
G3： インテリジェンス協働
形式手法グループ（石川）ソフトウェア工学，テスト，モデリ
ング，要求工学，…

機械学習・AID

E

ソフトウェア工学

CGroup 3

Group 1

A

（メタ）
数理的基盤
21

Group 0

学術研究の進捗状況
グループ間の協働の進展
新たな応用が導く理論発展
実行時監視
深層学習のための圏論的理論
機械学習利用 ➜ 効率的テスト
数理的基盤(G0)の重要性
学術的＆人的国際的 visibility:

学術研究で世界的先端を走るからこそ可能な産業応用

いわゆる「トップ国際会議」(CORE rank A, A*) 論文 > 30 報
最優秀論文賞： ICECCSʼ18, FoSSaCSʼ19（共にCORE rank A）
理論計算機科学の最高峰国際会議 LICSʼ19（CORE rank A*）では，全採択数 60 報のうち 6 報でERATO MMSD 研究者が（共）著者
22

応用上の進捗状況
プロトタイプツール多数
実行時監視ツールMONAA [Waga+, FORMATSʼ17] https://github.com/maswag/monaa
SyMon [Waga+, CAVʼ19] https://github.com/MasWag/symon
サーチベーステストツール
FalStar [Zhang+, EMSOFTʼ18] https://github.com/eratommsd/falstar
その他： 確率的プログラム自動検証ツール，RNN2WFA ツール（recurrent
neural network を重み付きオートマトンに近似），...
U Waterloo の自動運転プロジェクト autonomoose と協働，
形式手法の応用に向けて，具体的トピックについて研究推進中
国内の企業10社弱と共同研究・学術指導・定期的議論（自動車メーカー，自動車部品メーカー，総合電機メーカー，
ソフトウェアベンダーなど）

23

ところで：AI 研究の歴史（超ダイジェスト）
1980-1987 「論理的人工知能，エキスパートシステム」
与えられたルールによる論理的推論
判断の過程が明らかにトレースできる「与えられたルール」の準備が大変（人力ではおそらく不可能）
Prolog, 第５世代コンピュータ
関連する数学分野： 論理学，数学基礎論
2011-現在「統計的機械学習」
大量のデータから自動で統計的に特徴量抽出
驚くべきスケーラビリティ．
画像処理，物体認識，自動翻訳，…
判断の過程はブラックボックス
ディープニューラルネットワーク
関連する数学分野： 統計学，最適化
24sha1_base64="QU7R4MRdrzYV+ZABS7bL282TrJU=">AAACL3icbZDLSsNAFIYnXmu9Rd3pZrAorkoigi7bunFZwV6gKWUyPWmHTmbCzEQooeDTuFWfRtyIW19CTNostO2BgZ//P+cw5/MjzrRxnA9rZXVtfWOzsFXc3tnd27cPDptaxopCg0ouVdsnGjgT0DDMcGhHCkjoc2j5o9ssbz2C0kyKBzOOoBuSgWABo8SkVs8+xh4TAaikNkmq+BxXPR1HGgyuTXp2ySk708KLws1FCeVV79k/Xl/SOARhKCdad1wnMt2EKMMoh0nRizVEhI7IADqpFCQE3U2mN0zwWer0cSBV+oTBU/fvREJCrcehn3aGxAz1fJaZS7NISRksSzqxCW66CRNRbEDQ2ReCmGMjcYYK95kCavg4FYQqll6B6ZAoQk0KtOhlC3O0iS95PwPmzuNZFM3LsuuU3furUqWWoyugE3SKLpCLrlEF3aE6aiCKntAzekGv1pv1bn1aX7PWFSufOUL/yvr+BdgtqWc=</latexit>

sha1_base64="QU7R4MRdrzYV+ZABS7bL282TrJU=">AAACL3icbZDLSsNAFIYnXmu9Rd3pZrAorkoigi7bunFZwV6gKWUyPWmHTmbCzEQooeDTuFWfRtyIW19CTNostO2BgZ//P+cw5/MjzrRxnA9rZXVtfWOzsFXc3tnd27cPDptaxopCg0ouVdsnGjgT0DDMcGhHCkjoc2j5o9ssbz2C0kyKBzOOoBuSgWABo8SkVs8+xh4TAaikNkmq+BxXPR1HGgyuTXp2ySk708KLws1FCeVV79k/Xl/SOARhKCdad1wnMt2EKMMoh0nRizVEhI7IADqpFCQE3U2mN0zwWer0cSBV+oTBU/fvREJCrcehn3aGxAz1fJaZS7NISRksSzqxCW66CRNRbEDQ2ReCmGMjcYYK95kCavg4FYQqll6B6ZAoQk0KtOhlC3O0iS95PwPmzuNZFM3LsuuU3furUqWWoyugE3SKLpCLrlEF3aE6aiCKntAzekGv1pv1bn1aX7PWFSufOUL/yvr+BdgtqWc=</latexit><latexit

sha1_base64="QU7R4MRdrzYV+ZABS7bL282TrJU=">AAACL3icbZDLSsNAFIYnXmu9Rd3pZrAorkoigi7bunFZwV6gKWUyPWmHTmbCzEQooeDTuFWfRtyIW19CTNostO2BgZ//P+cw5/MjzrRxnA9rZXVtfWOzsFXc3tnd27cPDptaxopCg0ouVdsnGjgT0DDMcGhHCkjoc2j5o9ssbz2C0kyKBzOOoBuSgWABo8SkVs8+xh4TAaikNkmq+BxXPR1HGgyuTXp2ySk708KLws1FCeVV79k/Xl/SOARhKCdad1wnMt2EKMMoh0nRizVEhI7IADqpFCQE3U2mN0zwWer0cSBV+oTBU/fvREJCrcehn3aGxAz1fJaZS7NISRksSzqxCW66CRNRbEDQ2ReCmGMjcYYK95kCavg4FYQqll6B6ZAoQk0KtOhlC3O0iS95PwPmzuNZFM3LsuuU3furUqWWoyugE3SKLpCLrlEF3aE6aiCKntAzekGv1pv1bn1aX7PWFSufOUL/yvr+BdgtqWc=</latexit><latexit

sha1_base64="QU7R4MRdrzYV+ZABS7bL282TrJU=">AAACL3icbZDLSsNAFIYnXmu9Rd3pZrAorkoigi7bunFZwV6gKWUyPWmHTmbCzEQooeDTuFWfRtyIW19CTNostO2BgZ//P+cw5/MjzrRxnA9rZXVtfWOzsFXc3tnd27cPDptaxopCg0ouVdsnGjgT0DDMcGhHCkjoc2j5o9ssbz2C0kyKBzOOoBuSgWABo8SkVs8+xh4TAaikNkmq+BxXPR1HGgyuTXp2ySk708KLws1FCeVV79k/Xl/SOARhKCdad1wnMt2EKMMoh0nRizVEhI7IADqpFCQE3U2mN0zwWer0cSBV+oTBU/fvREJCrcehn3aGxAz1fJaZS7NISRksSzqxCW66CRNRbEDQ2ReCmGMjcYYK95kCavg4FYQqll6B6ZAoQk0KtOhlC3O0iS95PwPmzuNZFM3LsuuU3furUqWWoyugE3SKLpCLrlEF3aE6aiCKntAzekGv1pv1bn1aX7PWFSufOUL/yvr+BdgtqWc=</latexit><latexit<latexit

ERATO MMSD の研究開発の目標：
両者を組み合わせた高信頼物理情報システム

統計的機械学習 vs 演繹的形式推論
A

統計的機械学習
演繹的形式推論

データのノイズを 入力の
誤り
許容
公理は絶対
誤りは想定せず

保証されない結論の正しさ

論理的に保証

高い
スケーラ

低い

データから自動で特徴量発見

ビリティ
公理の準備は人力（cf. エキスパートシステム）

説明可
能性

高い

低い

判断の理由はパラメータ（重み）25（cf. 数学的証明）

推論過程が証明として明示的AB
B

アウトライン
ERATO MMSD プロジェクト概要
形式手法と物理情報システム
プロジェクトの研究開発状況
技術紹介
形式手法・テストによるシステム品質保証手法，特にサーチベーステスト
実行時監視
今後の協働に向けて
26

強化学習によるサーチベーステスト：
Simulink モデルの反例生成
throttle[Akazaki & Hasuo, CAV’15][Zhang, Ernst, Sedwards, Arcaini & Hasuo, EMSOFT’18][Zhang, Hasuo & Arcaini, CAV’19] …

speed
60
45
30
15
0

time
brake

0

10

20

30

10

20

30

RPM
70
52.5
35
17.5

time

0

0

ブラックボックステスト．
入出力の対応を見ながら，反例となる入力シグナルを探索
Given: Simulink モデル M， 時相論理仕様 φ
仕様 φ の例：
ギヤが4速になったらそれから3秒以内に時速 50 km/h 以上になる
目標：
出力シグナル M(i) が φ をみたさないような，入力シグナル i 27

強化学習によるサーチベーステスト：
Simulink モデルの反例生成[Akazaki & Hasuo, CAV’15][Zhang, Ernst, Sedwards, Arcaini & Hasuo, EMSOFT’18][Zhang, Hasuo & Arcaini, CAV’19] …

throttle

speed
60
45
30
15
0

time
brake

0

10

20

30

10

20

30

RPM
70
52.5
35
17.5
0

time

0

主流のアプローチ [Fainekos & Pappas, TCSʼ09]：
強化学習，確率的最適化で「あぶないところ」を狙う

more robustly
true

??

true

そのため，時相論理式φの真偽値を，ブール値（2値）から連続実数値に拡張 ➜ 勾配降下法

false

input

Boolean semantics

28

This way toclimb down :)less soquantitativerobust semantics

input強化学習によるサーチベーステスト：
Simulink モデルの反例生成[Akazaki & Hasuo, CAV’15][Zhang, Ernst, Sedwards, Arcaini & Hasuo, EMSOFT’18][Zhang, Hasuo & Arcaini, CAV’19] …

Survey: [Kapinski+, IEEE Control Syst. ʼ16]
J. Kapinski, J. V. Deshmukh, X. Jin, H. Ito, and K. Butts, “Simulation-based approaches for veriﬁcation of embedded control systems: An overview of
traditional and advanced modeling, testing, and veriﬁcation techniques,” IEEE Control Syst., vol. 36, no. 6, pp. 45‒64, Dec. 2016.

ERATO MMSD の貢献 [Zhang+, EMSOFTʼ18] を例に． [Zhang+, CAVʼ19]も同種のアイデア
確率的勾配降下法における離散構造の利用，
これによる反例発見能力の向上
モンテカルロ木探索

階層的最適化アーキテクチャ

離散最適化
探索結果を
フィードバック

探索領域を
指定

入力値の
領域の列
「ここから
探せ」

連続最適化
確率的勾配降下法（simulated annealing, CMA-ES など）
29

実行時監視： さまざまな定式化
Given: 離散時間ログ w = abaaacb…bbc
仕様 φ「b の後，6 step 待っても c が現れず」

時間的因果関係があり，そう簡単ではない

Answer: w の部分列でφを満たすもの全体
Given: 連続時間ログ w = (a, 0.12) (b, 1.28) …
仕様 φ 「b の後，6 秒待っても c が現れず」
Answer: w の部分列でφを満たすもの全体[Ulus, CAVʼ17] [Waga+, FORMATSʼ17] など

解は無限個（開始時刻は t=1? t = 1.01? t = 1.001? …)➜ 時間付きオートマトンの zone 構成で，効率的に表現・計算可能

Given: 連続時間ログ w = (a, 0.12) (b, 1.28) …
パラメータ付き仕様 φ(p) 「b の後，p 秒待っても c が現れず」「a は概ね p 秒周期で現れる」
Answer: (p, {w の部分列でφ(p)を満たすもの}) のペア全体[Waga+, ICECCSʼ18] [Waga+, NFMʼ19] [Waga+, CAVʼ19]など

30

実行時監視： ERATO MMSD の取り組み
時間付きオートマトンの理論による

Given: 離散時間ログ w = abaaacb…bbc
仕様 φ「b の後，6 step 待っても c が現れず」 高速アルゴリズム．ラップトップで毎秒，

Answer: w の部分列でφを満たすもの全体

数M の長さのログを処理[Waga+, FORMATSʼ17]https://github.com/maswag/monaa

Given: 連続時間ログ w = (a, 0.12) (b, 1.28) …

ルネサス RH850 実装もあり

仕様 φ 「b の後，6 秒待っても c が現れず」
Answer: w の部分列でφを満たすもの全体[Ulus, CAVʼ17] [Waga+, FORMATSʼ17] など

パラメータ・時間付きオートマトンの理論による高速アルゴリズム．ラップトップで毎秒，数十 K の長さのログを処理[Waga+, NFMʼ19]https://github.com/maswag/symon

Given: 連続時間ログ w = (a, 0.12) (b, 1.28) …
パラメータ付き仕様 φ(p) 「b の後，p 秒待っても c が現れず」「a は概ね p 秒周期で現れる」
Answer: (p, {w の部分列でφ(p)を満たすもの}) のペア全体[Waga+, ICECCSʼ18] [Waga+, NFMʼ19] [Waga+, CAVʼ19]など

31アウトライン
ERATO MMSD プロジェクト概要
形式手法と物理情報システム
プロジェクトの研究開発状況
技術紹介
形式手法・テストによるシステム品質保証手法，特にサーチベーステスト
実行時監視
今後の協働に向けて
32産学協働に向けて学術研究と産業応用は，研究推進の車の両輪．本気で取り組んでいます．スパイラル
いくつかのツールを公開しています
研究レベルのプロトタイプですが，ニーズに合わせて改良・適合が可能
論文リストから辿っていただけます
個別の共同研究・学術指導
具体的な課題を持ち込んでいただくと，話が早いです．
プロジェクトの持てる手法を総動員して解きます
自動運転をテーマにした研究会を組織する予定です（企業の方対象，今年度上半期）
定期セミナーで技術紹介，情報共有
先日のシンポジウム「高信頼自動運転システムのための先進的研究――数理的理論から，AI 協働，ソフトウェアプラットフォームへ」をきっかけに（ビデオ・スライド公開中）

くわしくは，ERATO MMSD プロジェクトウェブページまで！
https://group-mmm.org/eratommsd (「erato mmsd」で検索）
33