物理情報システムの信頼性保証
ソフトウェア科学から，制御理論・機械学習を包括する理論研究

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

アウトライン
ERATO MMSD プロジェクト：
物理情報システムの信頼性保証支援
形式手法 formal methods とは定理証明，モデル検査
形式手法と制御理論
物理情報システムへの実世界応用へ
技術紹介
サーチベーステスト，反例生成
モニタリング
形式安全アーキテクチャ
形式仕様記述支援
機械学習システムの信頼性保証．論理 vs 統計
プロジェクトの現状
2

Hasuo (NII, Tokyo)

ERATO MMSD 紹介
JST ERATO プロジェクト
2016/10-2022/03.
総勢50名規模の基礎研究プロジェクト
プロジェクト目標： 工業製品の設計サポート
形式手法の拡張．ソフトウェアから
物理情報システムへ
安全性・信頼性，Veriﬁcation & Validation．
「システムが期待通り動作するか」
対象： 自動車，交通システム，生産システム
医療システム，…
➜ IoT システム，Society 5.0
特に自動運転を戦略的ターゲットに．
U Waterloo と協働 www.autonomoose.net
3

Hasuo (NII, Tokyo)

今日の製造業における挑戦
複雑さの爆発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”
4automotiveit.eu

Hasuo (NII, Tokyo)

性能・機能が飛躍的に拡大，しかし今日の製造業に
工業製品の複雑さも飛躍的に拡大
おける挑戦

複雑さの爆発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”
5automotiveit.eu

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

Hasuo (NII, Tokyo)

アウトライン
ERATO MMSD プロジェクト：
物理情報システムの信頼性保証支援
形式手法 formal methods とは定理証明，モデル検査
形式手法と制御理論
物理情報システムへの実世界応用へ
技術紹介
サーチベーステスト，反例生成
モニタリング
形式安全アーキテクチャ
形式仕様記述支援
機械学習システムの信頼性保証．論理 vs 統計
プロジェクトの現状
7

Hasuo (NII, Tokyo)

形式手法

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)
8model

形式仕様記述speciﬁcation
Expressing aproperty desired ina formal language
machinerepresentablebasis for verif. &synthesis
Hasuo (NII, Tokyo)

形式検証の例１： 定理証明
例: 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
9

A Coq proof of ∀x. ¬P(x) → ¬ ∃x. P(x)Hasuo (NII, Tokyo)

ビジネスでの証明
オレが責任持つっす！

絶対大丈夫っす！

この駐車場，
どうっすか！？

．．．
（ダメだこいつ）

ホントに？ なんで？

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

ビジネスでの証明
はい，大丈夫です．
なぜなら，任意の状態 s に．．．（読んでる）
なるほど．それでは1
基いただこう．

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

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

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

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

b

a

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

b
a,b

👿

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

Hasuo (NII, Tokyo)

アウトライン
ERATO MMSD プロジェクト：
物理情報システムの信頼性保証支援
形式手法 formal methods とは定理証明，モデル検査
形式手法と制御理論
物理情報システムへの実世界応用へ
技術紹介
サーチベーステスト，反例生成
モニタリング
形式安全アーキテクチャ
形式仕様記述支援
機械学習システムの信頼性保証．論理 vs 統計
プロジェクトの現状
13

Hasuo (NII, Tokyo)

形式手法の歴史（超ダイジェスト）
ソフトウェアの大規模化

1970頃 形式手法によるソフトウェア品質保証（ソフトウェア検証）の研究開始．定理証明，モデル検査

ネットワー

1990頃 ソフトウェア検証のツール化・実応用加速

ク，分散並列定理証明： Isabelle, Coq, PVS, SMT solvers (Z3, …), …

物理システムモデル検査： SPIN, SMV/NuSMV, mCRL2, PRISM, Uppaal, …

との融合

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

Hasuo (NII, Tokyo)

形式検証の例１： 定理証明（再掲）
例: 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
15

A Coq proof of ∀x. ¬P(x) → ¬ ∃x. P(x)Hasuo (NII, Tokyo)

定理証明： 物理情報システムへ
物理情報システムに適用可能な例：
differential dynamic logic [Platzer]
André Platzer: Logical Foundations ofCyber-Physical Systems. Springer 2018

本質的に： Hoare 論理＋微分方程式
ツール： KeYmaera X
自動定理証明系として（自動証明モード）

KeYmaera X スクリーンショット

証明支援系として（対話証明モード）
実用上のチャレンジ： 論理体系が代数的厳密で，単純なホワイトボックスモデルが必要➜ 比較的単純なシステムの検証に応用が限られる
ブラックボックスコンポーネントや，外乱など，
不確かさのモデリングが容易ではない
16

参考： SpaceEx スクリーンショット
制度保証付き数値計算による可達性解析

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

b

a

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

b
a,b

👿

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

Hasuo (NII, Tokyo)

モデル検査： 物理情報システムへ
物理情報システムへの適用
一義的には，連続量が現れた時点でアウト
状態空間が無限になって，探索できない
例： ハイブリッド・オートマトン

ハイブリッド・オートマトンの例（オートマトン＋微分方程式）では，到達可能性が決定不能

from [Casau+, CDC’11]

確率的オートマトンならばOKMarkov chain, Markov decision process, …
到達可能性判定の代わりに，到達確率を計算する（線形計画法で解ける）
時間付きオートマトン timed automatonも OK
連続量の領域が，決まったテンプレート（region, zone）で記述できる
region, zone は有限個しかない

時間付きオートマトンと zone graph18

from [Daws+, FORMATS’06]

形式手法の歴史（超ダイジェスト，再掲）
ソフトウェアの大規模化

1970頃 形式手法によるソフトウェア品質保証（ソフトウェア検証）の研究開始．定理証明，モデル検査

ネットワー

1990頃 ソフトウェア検証のツール化・実応用加速

ク，分散並列定理証明： Isabelle, Coq, PVS, SMT solvers (Z3, …), …

物理システムモデル検査： SPIN, SMV/NuSMV, mCRL2, PRISM, Uppaal, …

との融合

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

Hasuo (NII, Tokyo)

制御理論 と 形式手法・ソフトウェア科学
対比
制御理論

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

連続空間・連続時間

対象システム

離散空間・離散時間

微分方程式

モデリング

オートマトン，プログラム

連続量最適化
LMI, SDP, …

最終的な
解き方

グラフアルゴリズム
SATソルバ，SMTソルバ

機械，電気

主な応用対象ソフトウェア

しかしワークフローは共通．「ダイナミクスを解きほぐす」
翻訳・帰着・変形ソフトウェア
検証問題

spec ↦ automaton
model ↦ prop. formula…

制約充足問題SATgraph reachability
…

最適化問題

制御問題

翻訳・帰着・変形

LMI
SDP

20

…

Hasuo (NII, Tokyo)

これまでの物理情報システム研究（特に安全性・信頼性の側面）
物理情報システム（特に hybrid system）
解析⇤(p ) ⌃q)<latexit sha1_base64="hv19xxln5Ihgt0PDz00mX3beYGs=">AAACF3icbZC7TsMwFIadcivlVmCEwaJCKkuVICQYq8LAWBC9SE1UOY7TWnXsYDtAFXXhLXgDVngBNsTKyM6D4LYZoOVIln79/znH9ufHjCpt219WbmFxaXklv1pYW9/Y3Cpu7zSVSCQmDSyYkG0fKcIoJw1NNSPtWBIU+Yy0/MH5OG/dEamo4Dd6GBMvQj1OQ4qRNla3uO/WxEM5dq9pr6+RlOLevaAoEjyAt0fdYsmu2JOC88LJRAlkVe8Wv91A4CQiXGOGlOo4dqy9FElNMSOjgpsoEiM8QD3SMZKjiCgvnfxiBA+NE8BQSHO4hhP390SKIqWGkW86I6T7ajYbm/9lnUSHZ15KeZxowvH0ojBhUAs4RgIDKgnWbGgEwpKat0LcRxJhbcAV3PHCDGHqCxaMDBZnFsK8aB5XHLviXJ2UqrUMUB7sgQNQBg44BVVwCeqgATB4BM/gBbxaT9ab9W59TFtzVjazC/6U9fkDl7ugSA==</latexit>

制御理論

形式手法
協働

x0 = f (x, u)<latexit sha1_base64="OLHwdpyatx3yKIFqo/K47yv4v90=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDIjgm6EohuXFexD2qFk0kwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy09cCFwzn3JveeIGJUG9f9cnJLyyura/n1wsbm1vZOcXevoWWsMKljyaRqBUgTRgWpG2oYaUWKIB4w0gyGN6nffCRKUynuzTgiPkd9QUOKkbHSw+j4KiyPTuOTbrHkVtwp4CLxMlICGWrd4nenJ3HMiTCYIa3bnhsZP0HKUMzIpNCJNYkQHqI+aVsqECfaT6YLT+CRVXowlMqWMHCq/p5IENd6zAPbyZEZ6HkvFf/z2rEJL/2Eiig2RODZR2HMoJEwvR72qCLYsLElCCtqd4V4gBTCxmZU6KQPZmklgWS9iY3Fmw9hkTTOKp5b8e7OS9XrLKA8OACHoAw8cAGq4BbUQB1gwMEzeAGvzpPz5rw7H7PWnJPN7IM/cD5/AH9Ul5E=</latexit>
sha1_base64="4LCzMseb0W4aHc9jzDSRRbHgPjA=">AAAB63icbZC7TsMwGIX/lFsJBcrMYlEhMVUJC4xILIxFoheprSrHcVqrjh3Zf5BK1Bdg5QXYEI/EzoPgtBmg5UiWjs7x5fcXZVJYDIIvr7azu7d/UD/0jxr+8clps9GzOjeMd5mW2gwiarkUindRoOSDzHCaRpL3o/l92fefubFCqydcZHyc0qkSiWAUXdSZNFtBO1iJbJuwMi2oNGl+j2LN8pQrZJJaOwyDDMcFNSiY5Et/lFueUTanUz50VtGU23GxGnNJLl0Sk0QbtxSSVfr7REFTaxdp5HamFGd2syvD/7phjsntuBAqy5Ertn4oySVBTco/k1gYzlAunKHMCDcrYTNqKENHxh+VF1aMikjLeOmohJsMtk3vuh0G7fAxgDqcwwVcQQg3cAcP0IEuMIjhFd68F+/d+1jTq3kVxjP4I+/zB6n+kjc=</latexit>
sha1_base64="wdgUGz0/4fuZ88hKGlj8zgUTtXk=">AAAB93icbZDLSgMxGIX/qbdaq1a3boJFrCBlxo1uBMGNywr2Iu1QMmmmDU0yQ5KRlqE738CtvoA78Wnc+yBm2llo64HA4Zxc/nxBzJk2rvvlFNbWNza3itulnfLu3n7loNzSUaIIbZKIR6oTYE05k7RpmOG0EyuKRcBpOxjfZn37iSrNIvlgpjH1BR5KFjKCjY0eJ6fXYW1ynpz1K1W37s6FVo2XmyrkavQr371BRBJBpSEca9313Nj4KVaGEU5npV6iaYzJGA9p11qJBdV+Oh94hk5sMkBhpOySBs3T3ydSLLSeisDuFNiM9HKXhf913cSEV37KZJwYKsnioTDhyEQo+z0aMEWJ4VNrMFHMzorICCtMjGVU6mUX5rTSIOKDmcXiLUNYNa2LuufWvXsXinAEx1ADDy7hBu6gAU0gIOAFXuHNeXbenY8FwIKTkzyEP3I+fwD4XJYk</latexit>
sha1_base64="Hx+nB8T5F5UCLoxoqCIXEBH+afA=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDLjRjdC0Y3LCvYh7VAymUwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy0euDC4Zx7k3tPEDOqjet+OoWl5ZXVteJ6aWNza3unvLvX0jJRmDSxZFJ1AqQJo4I0DTWMdGJFEA8YaQej68xvPxClqRR3ZhITn6OBoBHFyFjpfnx8GVXHp8lJv1xxa+4M8C/xclIBORr98lcvlDjhRBjMkNZdz42NnyJlKGZkWuolmsQIj9CAdC0ViBPtp7OFp/DIKiGMpLIlDJypPydSxLWe8MB2cmSGetHLxP+8bmKiCz+lIk4MEXj+UZQwaCTMrochVQQbNrEEYUXtrhAPkULY2IxKvezBPK00kCyc2li8xRD+ktZZzXNr3q1bqV/lARXBATgEVeCBc1AHN6ABmgADDp7AM3hxHp1X5815n7cWnHxmH/yC8/ENfhSXjQ==</latexit>

追いつかなければ…??

物理情報システム研究への取り組みでは欧米が先行
米国： NSF の CPS 研究イニシアチブ (2006-)
欧州： 形式手法の定量的拡張（確率，時間，…）
21

Hasuo (NII, Tokyo)

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

制御理論

形式手法

<latexit sha1_base64="hv19xxln5Ihgt0PDz00mX3beYGs=">AAACF3icbZC7TsMwFIadcivlVmCEwaJCKkuVICQYq8LAWBC9SE1UOY7TWnXsYDtAFXXhLXgDVngBNsTKyM6D4LYZoOVIln79/znH9ufHjCpt219WbmFxaXklv1pYW9/Y3Cpu7zSVSCQmDSyYkG0fKcIoJw1NNSPtWBIU+Yy0/MH5OG/dEamo4Dd6GBMvQj1OQ4qRNla3uO/WxEM5dq9pr6+RlOLevaAoEjyAt0fdYsmu2JOC88LJRAlkVe8Wv91A4CQiXGOGlOo4dqy9FElNMSOjgpsoEiM8QD3SMZKjiCgvnfxiBA+NE8BQSHO4hhP390SKIqWGkW86I6T7ajYbm/9lnUSHZ15KeZxowvH0ojBhUAs4RgIDKgnWbGgEwpKat0LcRxJhbcAV3PHCDGHqCxaMDBZnFsK8aB5XHLviXJ2UqrUMUB7sgQNQBg44BVVwCeqgATB4BM/gBbxaT9ab9W59TFtzVjazC/6U9fkDl7ugSA==</latexit>x0 = f (x, u)

協働<latexit sha1_base64="OLHwdpyatx3yKIFqo/K47yv4v90=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDIjgm6EohuXFexD2qFk0kwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy09cCFwzn3JveeIGJUG9f9cnJLyyura/n1wsbm1vZOcXevoWWsMKljyaRqBUgTRgWpG2oYaUWKIB4w0gyGN6nffCRKUynuzTgiPkd9QUOKkbHSw+j4KiyPTuOTbrHkVtwp4CLxMlICGWrd4nenJ3HMiTCYIa3bnhsZP0HKUMzIpNCJNYkQHqI+aVsqECfaT6YLT+CRVXowlMqWMHCq/p5IENd6zAPbyZEZ6HkvFf/z2rEJL/2Eiig2RODZR2HMoJEwvR72qCLYsLElCCtqd4V4gBTCxmZU6KQPZmklgWS9iY3Fmw9hkTTOKp5b8e7OS9XrLKA8OACHoAw8cAGq4BbUQB1gwMEzeAGvzpPz5rw7H7PWnJPN7IM/cD5/AH9Ul5E=</latexit>
sha1_base64="4LCzMseb0W4aHc9jzDSRRbHgPjA=">AAAB63icbZC7TsMwGIX/lFsJBcrMYlEhMVUJC4xILIxFoheprSrHcVqrjh3Zf5BK1Bdg5QXYEI/EzoPgtBmg5UiWjs7x5fcXZVJYDIIvr7azu7d/UD/0jxr+8clps9GzOjeMd5mW2gwiarkUindRoOSDzHCaRpL3o/l92fefubFCqydcZHyc0qkSiWAUXdSZNFtBO1iJbJuwMi2oNGl+j2LN8pQrZJJaOwyDDMcFNSiY5Et/lFueUTanUz50VtGU23GxGnNJLl0Sk0QbtxSSVfr7REFTaxdp5HamFGd2syvD/7phjsntuBAqy5Ertn4oySVBTco/k1gYzlAunKHMCDcrYTNqKENHxh+VF1aMikjLeOmohJsMtk3vuh0G7fAxgDqcwwVcQQg3cAcP0IEuMIjhFd68F+/d+1jTq3kVxjP4I+/zB6n+kjc=</latexit>
sha1_base64="wdgUGz0/4fuZ88hKGlj8zgUTtXk=">AAAB93icbZDLSgMxGIX/qbdaq1a3boJFrCBlxo1uBMGNywr2Iu1QMmmmDU0yQ5KRlqE738CtvoA78Wnc+yBm2llo64HA4Zxc/nxBzJk2rvvlFNbWNza3itulnfLu3n7loNzSUaIIbZKIR6oTYE05k7RpmOG0EyuKRcBpOxjfZn37iSrNIvlgpjH1BR5KFjKCjY0eJ6fXYW1ynpz1K1W37s6FVo2XmyrkavQr371BRBJBpSEca9313Nj4KVaGEU5npV6iaYzJGA9p11qJBdV+Oh94hk5sMkBhpOySBs3T3ydSLLSeisDuFNiM9HKXhf913cSEV37KZJwYKsnioTDhyEQo+z0aMEWJ4VNrMFHMzorICCtMjGVU6mUX5rTSIOKDmcXiLUNYNa2LuufWvXsXinAEx1ADDy7hBu6gAU0gIOAFXuHNeXbenY8FwIKTkzyEP3I+fwD4XJYk</latexit>
sha1_base64="Hx+nB8T5F5UCLoxoqCIXEBH+afA=">AAACAnicbVDLSgMxFM3UV62vqks3wSJWkDLjRjdC0Y3LCvYh7VAymUwbmseQZKRl6M4/cKs/4E7c+iPu/RAz7Sy0euDC4Zx7k3tPEDOqjet+OoWl5ZXVteJ6aWNza3unvLvX0jJRmDSxZFJ1AqQJo4I0DTWMdGJFEA8YaQej68xvPxClqRR3ZhITn6OBoBHFyFjpfnx8GVXHp8lJv1xxa+4M8C/xclIBORr98lcvlDjhRBjMkNZdz42NnyJlKGZkWuolmsQIj9CAdC0ViBPtp7OFp/DIKiGMpLIlDJypPydSxLWe8MB2cmSGetHLxP+8bmKiCz+lIk4MEXj+UZQwaCTMrochVQQbNrEEYUXtrhAPkULY2IxKvezBPK00kCyc2li8xRD+ktZZzXNr3q1bqV/lARXBATgEVeCBc1AHN6ABmgADDp7AM3hxHp1X5815n7cWnHxmH/yC8/ENfhSXjQ==</latexit>

課題： 実システムに対するスケーラビリティ
ホワイトボックスモデルの完全な理解が前提

可能？
役に立つ？

結論の数学的正しさを絶対視
不確かさを許容する余地が少ない ➜ 統計的機械学習との相性の問題
22

Hasuo (NII, Tokyo)

アウトライン
ERATO MMSD プロジェクト：
物理情報システムの信頼性保証支援
形式手法 formal methods とは定理証明，モデル検査
形式手法と制御理論
物理情報システムへの実世界応用へ
技術紹介
サーチベーステスト，反例生成
モニタリング
形式安全アーキテクチャ
形式仕様記述支援
機械学習システムの信頼性保証．論理 vs 統計
プロジェクトの現状
23

Hasuo (NII, Tokyo)

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

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

テスト test

自動定理証明

モデル検査
低

コスト

ブラックボックス

対話定理証明高

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

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

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

高低保証の数学的厳密性

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

Hasuo (NII, Tokyo)

スケールダウンできない形式手法
形式手法（特に形式検証）の多くはスケールダウンできない
ホワイトボックスモデルを要求．
全てのコンポーネントの形式モデル

品質保証の度合い

数学的証明 ➜
品質保証度は高い

既存の設計プロセスの刷新を要求
品質保証が非ゼロになるまでのコストが莫大
物理情報システムへの適用例：
航空機（エアバス），宇宙開発（NASA），...
失敗のコストが莫大であり，コストをかけてもペイする

コスト
ホワイトボックスモデルの作成コスト

それでも数十年単位の取り組み
物理系の融合は困難➜ ソフトウェアの側面に注力
25

Hasuo (NII, Tokyo)

スケールダウンできる形式手法へ
自動車などの実製品への応用では，「スケールダウンできること」
が重要半分のコストしかかけられない
場合に，品質保証の度合い✘✔

品質保証度合いがゼロではな
く，半分でも得られるように
コスト

26

Hasuo (NII, Tokyo)

アウトライン
ERATO MMSD プロジェクト：
物理情報システムの信頼性保証支援
形式手法 formal methods とは定理証明，モデル検査
形式手法と制御理論
物理情報システムへの実世界応用へ
技術紹介
サーチベーステスト，反例生成
モニタリング
形式安全アーキテクチャ
形式仕様記述支援
機械学習システムの信頼性保証．論理 vs 統計
プロジェクトの現状
27

Hasuo (NII, Tokyo)

強化学習によるサーチベーステスト：
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
0

time

0

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

Hasuo (NII, Tokyo)

強化学習によるサーチベーステスト：
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

??

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

true
false

input

Boolean semantics

This way toclimb down :)less so

input

quantitativerobust semantics

Hasuo (NII, Tokyo)

強化学習によるサーチベーステスト：
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

ユースケースブラックボックステスト．効率的にバグを発見
システムモデルは Simulink でなくてもよい．
Hardware-in-the-Loop でも可
注： 検証ではない．「バグが存在しないこと」は結論できない
制御器生成
30

Hasuo (NII, Tokyo)

強化学習によるサーチベーステスト：
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 など）
31

Hasuo (NII, Tokyo)

アウトライン
ERATO MMSD プロジェクト：
物理情報システムの信頼性保証支援
形式手法 formal methods とは定理証明，モデル検査
形式手法と制御理論
物理情報システムへの実世界応用へ
技術紹介
サーチベーステスト，反例生成
モニタリング
形式安全アーキテクチャ
形式仕様記述支援
機械学習システムの信頼性保証．論理 vs 統計
プロジェクトの現状
32

Hasuo (NII, Tokyo)

モニタリング： さまざまな定式化
関連トピック（しばしば同義語？）：
実行時検証，実行時監視，パターンマッチング，…
Given: 離散時間ログ w = abaaacb…bbc
仕様 φ「b の後，6 step 待っても c が現れず」
Answer: w の部分列でφを満たすもの全体
簡単？
… 時間的因果関係があり，そう簡単ではない

ユースケース
集めた大量のログの解析「面白いところだけ見たい」
実行時監視「危ないときにアラート」
33

Hasuo (NII, Tokyo)

モニタリング： さまざまな定式化
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]など

34

Hasuo (NII, Tokyo)

形式検証の例２： モデル検査
物理情報システムへの適用
一義的には，連続量が現れた時点でアウト
状態空間が無限になって，探索できない
例： ハイブリッド・オートマトン

ハイブリッド・オートマトンの例
from [Casau+, CDC’11]（オートマトン＋微分方程式）では，到達可能性が決定不能• 再掲

確率的オートマトンならばOKMarkov chain, Markov decision process, …
到達可能性判定の代わりに，到達確率を計算する（線形計画法で解ける）
時間付きオートマトン timed automatonも OK
連続量の領域が，決まったテンプレート（region, zone）で記述できる
region, zone は有限個しかない

時間付きオートマトンと zone graph

35

from [Daws+, FORMATS’06]

モニタリング： 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 & CAVʼ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]など

36

Hasuo (NII, Tokyo)

モニタリング： ERATO MMSD の取り組み (2/2)

Naive Remote Monitor

フィルタリングによる前処理[Waga & Hasuo, EMSOFTʼ18]

SensorMonitorContribution: Filter for Remote Monitor
組み込み
チップ

SensorFilter
高速な逐次機械（ムーアマシン）
でログの無駄な部分をフィルタ

Monitorアウトライン
ERATO MMSD プロジェクト：
物理情報システムの信頼性保証支援
形式手法 formal methods とは定理証明，モデル検査
形式手法と制御理論
物理情報システムへの実世界応用へ
技術紹介
サーチベーステスト，反例生成
モニタリング
形式安全アーキテクチャ
形式仕様記述支援
機械学習システムの信頼性保証．論理 vs 統計
プロジェクトの現状
38

Hasuo (NII, Tokyo)

ERATO MMSD の研究開発の目標：
これらの柔軟なミックス ➜ 実システムへ応用
特に： 定理証明をスケールダウンするためにソフトウェア品質保証におけるスペクトル （再掲）は？
形式手法

テスト test

自動定理証明

モデル検査
低

コスト

ブラックボックス

対話定理証明高

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

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

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

高低保証の数学的厳密性

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

Hasuo (NII, Tokyo)

arXiv:1704.04759v1 [cs.SY] 16 Apr 201

Abstract—We present Component-Based Simplex Architecture(CBSA), a new framework for assuring the runtime safety ofcomponent-based cyber-physical systems (CPSs). CBSA integrates Assume-Guarantee (A-G) reasoning with the core principles of the Simplex control architecture to allow component-based
CPSs to run advanced, uncertified controllers while still providing
runtime assurance that A-G contracts and global properties are
satisfied. In CBSA, multiple Simplex instances, which can becomposed in a nested, serial or parallel manner, coordinate toassure system-wide properties.
Combining A-G reasoning and the Simplex architecture is achallenging problem that yields significant benefits. By utilizing
A-G contracts, we are able to compositionally determine theswitching logic for CBSAs, thereby alleviating the state explosion
encountered by other approaches. Another benefit is that we
can use A-G proof rules to decompose the proof of system-widesafety assurance into sub-proofs corresponding to the componentbased structure of the system architecture. We also introduce thenotion of coordinated switching between Simplex instances, a key
component of our compositional approach to reasoning about
CBSA switching logic.
We illustrate our framework with a component-based control
system for a ground rover. We formally prove that the CBSA for
this system guarantees energy safety (the rover never runs outof power), and collision freedom (the rover never collides witha stationary obstacle). We also consider a CBSA for the roverthat guarantees mission completion: all target destinations visited
within a prescribed amount of time.
Index Terms—Simplex architecture; Assume-guarantee reasoning; Component-based system architecture; Cyber-physicalsystems; Collision avoidanceAs such, Simplex is a very powerful architecture. It assuresthat the plant is properly controlled even if the advanced controller has bugs. As advanced controllers are increasingly more
complex, more adaptive with the use of unverified algorithms
such as machine-learning’s, runtime assurance techniques like
Simplex are becoming more important. Figure 1 illustrates the
Simplex architecture.

形式安全アーキテクチャ
安全アーキテクチャの例：
simplex architecture （右図）

通常系（AC）は
複雑，性能重視，ブラックボックス

Phanet al.,and
ACSD’17
Fig. 1. The Simplex architecture. The Decision
ModuleBaseline
保証系（BC）はController are pre-certified.
単純，安全性重視，（できるだけ）ホワイトボックス
The Simplex architecture was developed 20 years ago. Since

then, control systems have evolved to take on a more complex
structure consisting of multiple controllers, each with a distinct
functionality. For example, an autonomous vehicle might have
ポイント： AC がブラックボックスであっても，システム全体を形式検証できる．
a hierarchical control system consisting of controllers for (inorder of decreasing level of abstraction) mission-planning,
BC の安全性 及び DM （スイッチング戦略）の正しさが示せれば十分
guidance, navigation, and inner-loop control. A system ofthis form is illustrated in Fig. 2. Furthermore, some of theseI. I NTRODUCTION
controllers themselves may have a hierarchical or nested
仮に形式検証が不可能でも，システム設計・テストの系統的指針を与える
Simplex [1]–[3] is a software architecture for high-assurance structure.
Advanced control systems are not necessarily hierarchical,
process-control systems. It traditionally consists of a physical plant and two versions of the controller: an advanced but are better understood as having a component-based arcontroller (AC) and a baseline controller (BC). The AC is chitecture. A “component” may be a software module or the
留意点： 冗長性，独立性，多様性，…
in control of the plant under nominal operating conditions, distinguished physical-plant node (we do not consider multiple
and is designed to achieve high-performance according to physical plants, because a physical plant can be arbitrarily
certain metrics (e.g., maneuverability, fuel economy, mission- complex). It is important to have runtime assurance techniques
ユースケース：completion time). The BC is pre-certified to keep the plant for component-based control systems that are equally modular,
within a prescribed safety region, i.e., a region of safe op- to reduce their associated complexity and cost.
テスト以上の保証度合いが必要な，safety-criticalの品質保証
eration. A decision module (DM), which is also pre-certified, system
Components
may have different update periods (or excontinually monitors the state of the plant and 40
switches control ecution periods). For the autonomous-vehicle example, theof the plant to the BC should the plant be in imminent danger mission-planning component’s update period may be a multi-

arXiv:1704.04759v1 [cs.SY] 16 Apr 20

Abstract—We present Component-Based Simplex Architecture(CBSA), a new framework for assuring the runtime safety ofcomponent-based cyber-physical systems (CPSs). CBSA integrates Assume-Guarantee (A-G) reasoning with the core principles of the Simplex control architecture to allow component-based
CPSs to run advanced, uncertified controllers while still providing
runtime assurance that A-G contracts and global properties are
satisfied. In CBSA, multiple Simplex instances, which can becomposed in a nested, serial or parallel manner, coordinate toassuresystem-wide
properties.
ERATO
MMSD
の取り組み：
Combining A-G reasoning and the Simplex architecture is achallenging problem that yields significant benefits. By utilizing
安全アーキテクチャのA-G contracts, we are able to compositionally determine theswitching logic for CBSAs, thereby alleviating the state explosion
Event-Bencountered による形式化
by other approaches. Another benefit is that we
can use A-G proof rules to decompose the proof of system-widesafety assurance into sub-proofs corresponding to the componentbased structure of the system architecture. We also introduce theEvent-B:
notion 形式モデリングツール
of coordinated switching between Simplex instances, a key
componentof ourcompositional[Abrial, “TheEvent-B
Book”,
2010 CUP]approach to reasoning about
CBSA switching logic.
[Kobayashi+,
WeICFEMʼ18]など
illustrate our framework with a component-based control
system for a ground rover. We formally prove that the CBSA for
状態遷移系を基礎とする．次をサポート
this system guarantees energy safety (the rover never runs outof power), and collision freedom (the rover never collides witha stationary obstacle). We also consider a CBSA for the rover
安全性証明
that guarantees mission completion: all target destinations visited
within a prescribed amount of time.
SMT
ソルバによる自動証明など
Index
Terms—Simplex
architecture; Assume-guarantee reasoning; Component-based system architecture; Cyber-physicalsystems;
Collision avoidance
コンポーネント間の契約に基づく，

As such, Simplex is a very powerful architecture. It assuresthat the plant is properly controlled even if the advanced controller has bugs. As advanced controllers are increasingly more
complex, more adaptive with the use of unverified algorithms
such as machine-learning’s, runtime assurance techniques like
Simplex are becoming more important. Figure 1 illustrates the
Simplex architecture.

形式安全アーキテクチャ

Phan
et al.,and
ACSD’17
Fig. 1. The Simplex architecture. The Decision
ModuleBaseline
Controller are pre-certified.

The Simplex architecture was developed 20 years ago. Since
then, control systems have evolved to take on a more complex
structure consisting of multiple controllers, each with a distinct
functionality. For example, an autonomous vehicle might havea hierarchical control system consisting of controllers for (inorder of decreasing level of abstraction) mission-planning,
guidance, navigation, and inner-loop control. A system ofthis form is illustrated in Fig. 2. Furthermore, some of theseI. I NTRODUCTION
controllers themselves may have a hierarchical or nested
assume-guarantee型推論 ➜ ブラックボックスを許容
Simplex [1]–[3] is a software architecture for high-assurance structure.
Advanced control systems are not necessarily hierarchical,
process-control
systems. It traditionally consists of a phys契約が履行されるかのチェックには，モニタリングが使える
ical plant and two versions of the controller: an advanced but are better understood as having a component-based arcontroller (AC) and a baseline controller (BC). The AC is chitecture. A “component” may be a software module or the
モデルの段階的詳細化をサポート
in control of the plant under nominal operating conditions, distinguished physical-plant node (we do not consider multiple
and isdesigned to achieve high-performance according to physical plants, because a physical plant can be arbitrarily
個別のアーキテクチャの体系的導出に使える
certain metrics (e.g., maneuverability, fuel economy, mission- complex). It is important to have runtime assurance techniques
41
completion time). The BC is pre-certified to keep the plant for component-based control systems that are equally modular,

arXiv:1704.04759v1 [cs.SY] 16 Apr 20

Abstract—We present Component-Based Simplex Architecture(CBSA), a new framework for assuring the runtime safety ofcomponent-based cyber-physical systems (CPSs). CBSA integrates Assume-Guarantee (A-G) reasoning with the core principles of the Simplex control architecture to allow component-based
CPSs to run advanced, uncertified controllers while still providing
runtime assurance that A-G contracts and global properties are
satisfied. In CBSA, multiple Simplex instances, which can becomposed in a nested, serial or parallel manner, coordinate toassure system-wide properties.
Combining A-G reasoning and the Simplex architecture is achallenging problem that yields significant benefits. By utilizing
A-G contracts, we are able to compositionally determine theswitching logic for CBSAs, thereby alleviating the state explosion
encountered by other approaches. Another benefit is that we
can use A-G proof rules to decompose the proof of system-widesafety assurance into sub-proofs corresponding to the componentbased structure of the system architecture. We also introduce thenotion of coordinated switching between Simplex instances, a key
component of our compositional approach to reasoning about
CBSA switching logic.
We illustrate our framework with a component-based control
system for a ground rover. We formally prove that the CBSA for
this system guarantees energy safety (the rover never runs outof power), and collision freedom (the rover never collides witha stationary obstacle). We also consider a CBSA for the roverthat guarantees mission completion: all target destinations visited
within a prescribed amount of time.
Index Terms—Simplex architecture; Assume-guarantee reasoning; Component-based system architecture; Cyber-physicalsystems; Collision avoidanceAs such, Simplex is a very powerful architecture. It assuresthat the plant is properly controlled even if the advanced controller has bugs. As advanced controllers are increasingly more
complex, more adaptive with the use of unverified algorithms
such as machine-learning’s, runtime assurance techniques like
Simplex are becoming more important. Figure 1 illustrates the
Simplex architecture.

形式安全アーキテクチャ
ERATO MMSD の取り組み：

安全アーキテクチャの Event-B
による形式化

現在の具体的取組み

自動運転システムのための，一般的安全アーキテクチャを構築，その信頼性を確認（autonomoose と協働，
自動運転独自のニーズを反映）
I. I NTRODUCTION

Simplex [1]–[3] is a software architecture for high-assurance
process-control systems. It traditionally consists of a physical plant and two versions of the controller: an advanced
controller (AC) and a baseline controller (BC). The AC isin control of the plant under nominal operating conditions,and is designed to achieve high-performance according tocertain metrics (e.g., maneuverability, fuel economy, mission42
completion time). The BC is pre-certified to keep the plant

一般的安全アーキテクチャから，企業さまの個別ニーズに応える個
別安全アーキテクチャを導出

Phanet al.,and
ACSD’17
Fig. 1. The Simplex architecture. The Decision
ModuleBaseline
Controller are pre-certified.

The Simplex architecture was developed 20 years ago. Since
then, control systems have evolved to take on a more complex
structure consisting of multiple controllers, each with a distinct
functionality. For example, an autonomous vehicle might havea hierarchical control system consisting of controllers for (inorder of decreasing level of abstraction) mission-planning,
guidance, navigation, and inner-loop control. A system ofthis form is illustrated in Fig. 2. Furthermore, some of thesecontrollers themselves may have a hierarchical or nested
structure.
Advanced control systems are not necessarily hierarchical,
but are better understood as having a component-based architecture. A “component” may be a software module or the
distinguished physical-plant node (we do not consider multiple
physical plants, because a physical plant can be arbitrarily
complex). It is important to have runtime assurance techniques
for component-based control systems that are equally modular,アウトライン
ERATO MMSD プロジェクト：
物理情報システムの信頼性保証支援
形式手法 formal methods とは定理証明，モデル検査
形式手法と制御理論
物理情報システムへの実世界応用へ
技術紹介
サーチベーステスト，反例生成
モニタリング
形式安全アーキテクチャ
形式仕様記述支援
機械学習システムの信頼性保証．論理 vs 統計
プロジェクトの現状
43

Hasuo (NII, Tokyo)

形式仕様記述を支援する対話型ツール• いきなり正しいものを書く
Slide by Alexandre Donzeのは困難
STL Examples• しかし，正解はエンジニアさ
Always |x| > 0.5 ∆ after 1 s, |x| settles under 0.5 for 1.5 s
んの頭の中！
mmÏ := G(x[t]40> .5 æ F[0,.6]
60 ( G[0,1.5] x[t]80 < 0.5)) 100
120• ➜形式仕様記述を支援する対話型ツール• 正例・反例を例示
cf. [Prabhakar+,
RTSSʼ18]• ユーザーのフィードバックを受けて，改訂をsuggest

40

60

0.5

0.5

0.5

•
80

Alexandre Donzé

Æ1 s

1.5 s

Æ1 s

1.5 s

Æ1 s

1.5 s

研究推進中
予備的成果： [Arcaini+, Softw. Test., Verif.
Reliab.ʼ19, ICTSSʼ18, arxiv 1907.02133]• 対面でのコンサルテーションも行っていますSignal Temporal Logic

44

EECS294-98 Spring 201412 / 52

Cf.
regex101
.com

試行 ➜
結果を表示
「なぜそう
なるか」
の説明

45

アウトライン
ERATO MMSD プロジェクト：
物理情報システムの信頼性保証支援
形式手法 formal methods とは定理証明，モデル検査
形式手法と制御理論
物理情報システムへの実世界応用へ
技術紹介
サーチベーステスト，反例生成
モニタリング
形式安全アーキテクチャ
形式仕様記述支援
機械学習システムの信頼性保証．論理 vs 統計
プロジェクトの現状
46

Hasuo (NII, Tokyo)

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

統計的機械学習 vs 演繹的形式推論
A<latexit sha1_base64="QU7R4MRdrzYV+ZABS7bL282TrJU=">AAACL3icbZDLSsNAFIYnXmu9Rd3pZrAorkoigi7bunFZwV6gKWUyPWmHTmbCzEQooeDTuFWfRtyIW19CTNostO2BgZ//P+cw5/MjzrRxnA9rZXVtfWOzsFXc3tnd27cPDptaxopCg0ouVdsnGjgT0DDMcGhHCkjoc2j5o9ssbz2C0kyKBzOOoBuSgWABo8SkVs8+xh4TAaikNkmq+BxXPR1HGgyuTXp2ySk708KLws1FCeVV79k/Xl/SOARhKCdad1wnMt2EKMMoh0nRizVEhI7IADqpFCQE3U2mN0zwWer0cSBV+oTBU/fvREJCrcehn3aGxAz1fJaZS7NISRksSzqxCW66CRNRbEDQ2ReCmGMjcYYK95kCavg4FYQqll6B6ZAoQk0KtOhlC3O0iS95PwPmzuNZFM3LsuuU3furUqWWoyugE3SKLpCLrlEF3aE6aiCKntAzekGv1pv1bn1aX7PWFSufOUL/yvr+BdgtqWc=</latexit>

統計的機械学習

演繹的形式推論

データのノイズを 入力の
誤り
許容

公理は絶対
誤りは想定せず

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

論理的に保証

高い

スケーラ

低い

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

ビリティ

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

説明可
能性

高い

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

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

A
B

BKey: 論理と統計的学習の間で，機械学習システムの安全性・信頼性保証
統計的
機械学習

帰納的
（データから学ぶ）

制御理論・
形式手法

演繹的
（証明）

システムレベルのタスク切り分けと構造化

不確かさ
ブラックボックス（データのノイズ）
数学的・論理的厳密性

ホワイトボックス

総当たり探索の代わりに，
データから傾向を読み取り高速に証明や補題を探索

制御理論・

統計的

形式手法

機械学習
不確かな機械学習コンポーネントを包み込む “safety envelope”
例： 自動運転の経路計画．safety
envelope の中で最適化
49

Hasuo (NII, Tokyo)

アウトライン
ERATO MMSD プロジェクト：
物理情報システムの信頼性保証支援
形式手法 formal methods とは定理証明，モデル検査
形式手法と制御理論
物理情報システムへの実世界応用へ
技術紹介
サーチベーステスト，反例生成
モニタリング
形式安全アーキテクチャ
形式仕様記述支援
機械学習システムの信頼性保証．論理 vs 統計
プロジェクトの現状
50

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 に集約
多様な背景： 論理学・代数学から形式手法，制御理論，機械学習，ソフトウェア工学まで
51
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の場合
応用

F

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

機械学習・AI

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

D

B
E

制御理論

C

ソフトウェア工学

A

基礎

（メタ）
数理的基盤
53

Hasuo (NII, Tokyo)

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

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

機械学習・AID

E

ソフトウェア工学

CGroup 3

Group 1

A

（メタ）
数理的基盤
54

GroupHasuo
0 (NII, Tokyo)

学術研究の進捗状況
グループ間の協働の進展
新たな応用が導く理論発展
モニタリング
深層学習のための圏論的理論
機械学習利用 ➜ 効率的テスト
聞き上手な理論家の雇用，
数理的基盤(G0)の重要性おすすめです学術的＆人的国際的 visibility:

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

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

Hasuo (NII, Tokyo)

応用上の進捗状況
プロトタイプツール多数
実行時監視ツール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社弱と共同研究・学術指導・定期的議論（自動車メーカー，自動車部品メーカー，総合電機メーカー，ソフトウェアベンダーなど）
56

Hasuo (NII, Tokyo)

産学協働の現状
学術研究と産業応用は，研究推進の車の両輪．
テーマ： 自動車に限らず，ロボット，生産システムなどから，機械学習システム，ソフトウェアまで
いくつかのツールを公開しています
研究レベルのプロトタイプですが，ニーズに合わせて改良・適合が可能
論文リストから辿っていただけます
研究会を組織する予定です（企業の方対象，今年度上半期）
定期セミナーで技術紹介，情報共有
先日のシンポジウム「高信頼自動運転システムのための先進的研究――数理的理論から，AI 協働，ソフトウェアプラットフォームへ」をきっかけに（ビデオ・スライド公開中）

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

Hasuo (NII, Tokyo)

まとめ
品質保証の度合い

Society 5.0 に向けた，物理情報システムの信頼性保証
従来ソフトウェアを対象としていた形式手法を，✘✔

制御理論と組み合わせ，物理情報システムへ適用
ブラックボックスモデル，統計的機械学習など，

コスト

実用上の課題➜ テストとの有機的組み合わせ
ERATO MMSD プロジェクト：
先端的学術研究と産業応用の上向きスパイラル「スケールダウンできる形式手法」
今すぐ使える技術多数．
既存の設計過程に寄り添う（サーチベーステスト，モニタリング，…）
設計過程の新パラダイムの提案も（形式安全アーキテクチャ，…）… 新しいチャレンジ ➜ 分野間協働，それをささえる数学的基盤
58

Hasuo (NII, Tokyo)