Quality Assurance ofCyber-Physical Systems
Mathematical Metatheory, Machine Learning and Automated Driving

物理情報システム研究の新地平
自動運転や機械学習をも包括する数学的基盤

Slides available:
bit.ly/2SdJpIY

Ichiro Hasuo

蓮尾 一郎

National Institute of Informatics, SOKENDAIERATO HASUO Metamathematics for Systems Design Project

On ERATO MMSDJST ERATO Project, 2016/10-2022/03
Our goal:formal methods for cyber-physical systems (CPS)
Extend formal methods, from software to CPS
Safety, reliability, V&V (Verification & Validation).
“Check if a system behaves as expected”
Automated driving as a strategic target domain.
Collaboration with U Waterloo: www.autonomoose.net
Our principle: broaden the realm of CPS research
Theory:abstract mathematical metatheory➜ scale out to diverse applications

CPSresearch

Practice: real-world systems (not only toy examples)
2Hasuo (NII, Tokyo)

On ERATO MMSDJST ERATO Project, 2016/10-2022/03
Our goal:formal methods for cyber-physical systems (CPS)
Extend formal methods, from software to CPS
Safety, reliability, V&V (Verification & Validation).
“Check if a system behaves as expected”
Automated driving as a strategic target domain.
Collaboration with U Waterloo: www.autonomoose.net
Our principle: broaden the realm of CPS research
Theory:abstract mathematical metatheory➜ scale out to diverse applications

CPSresearch

Practice: real-world systems (not only toy examples)
2Hasuo (NII, Tokyo)

Our Organization
International and multi-disciplinary. “creative chaos”
Group 0 @ NII:
Metatheoretical Integration
Leader: Shin-ya Katsumata

Kyoto U RIMS Site:
Categorical
Infrastructure
Leader:Masahito Hasegawa

Featured today:
Kenta Cho
Clovis Eberhart
Natsuki UrabeKyushu U Site:
Optimization for
CPS V&VLeader:
Hayato WakiGroup 3 @ NII:
Formal Methods andIntelligence
Leader: Fuyuki Ishikawa
Featured today:
Masaki Waga
Paolo Arcaini

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

Osaka U Site:
Control Theory forCPS
Leader:Toshimitsu Ushio

Group 1 @ NII:
Heterogeneous Formal Methods
Leader: Ichiro Hasuo
Featured today:
Etienne Andre
Akihisa Yamada
Toru Takisaka
Chao Huang

Hasuo (NII, Tokyo)

Cyber-Physical Systems：
Control Theory and Formal Methods/Software Science
Cyber-Physical System (CPS)“A mechanism that is controlled or monitored by computer-based algorithms,tightly integrated with the Internet and its users” (Wikipedia)
Physical plant (continuous) + Digital control (discrete)
In US: NSF Key Area of Research (2006-)
Formal methods: Logical proofs for “correctness” of (discrete) programs
Model checking [Pnueli, Clarke, Emerson, Sifakis, …]Theorem Proving (Coq, Agda, …) [Milner, Coquand, Leroy, Voevodsky, …]
Control Theory: Analysis of continuous dynamics
Stability, Lyapunov function, …
Their similarity is widely recognizedToru Takisaka’s talk on martingale synthesisfor probabilistic programs (later)
4CPS Research, So Far(the V&V Aspect)
CPS(esp. hybrid systems)
Analysis⇤(p ) ⌃q)<latexit sha1_base64="hv19xxln5Ihgt0PDz00mX3beYGs=">AAACF3icbZC7TsMwFIadcivlVmCEwaJCKkuVICQYq8LAWBC9SE1UOY7TWnXsYDtAFXXhLXgDVngBNsTKyM6D4LYZoOVIln79/znH9ufHjCpt219WbmFxaXklv1pYW9/Y3Cpu7zSVSCQmDSyYkG0fKcIoJw1NNSPtWBIU+Yy0/MH5OG/dEamo4Dd6GBMvQj1OQ4qRNla3uO/WxEM5dq9pr6+RlOLevaAoEjyAt0fdYsmu2JOC88LJRAlkVe8Wv91A4CQiXGOGlOo4dqy9FElNMSOjgpsoEiM8QD3SMZKjiCgvnfxiBA+NE8BQSHO4hhP390SKIqWGkW86I6T7ajYbm/9lnUSHZ15KeZxowvH0ojBhUAs4RgIDKgnWbGgEwpKat0LcRxJhbcAV3PHCDGHqCxaMDBZnFsK8aB5XHLviXJ2UqrUMUB7sgQNQBg44BVVwCeqgATB4BM/gBbxaT9ab9W59TFtzVjazC/6U9fkDl7ugSA==</latexit>

FormalMethods

Col

labo

Control
Theoryx0 = 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>

ration5

CPS Research, So Far(the V&V Aspect)
CPS(esp. hybrid systems)
Analysis⇤(p ) ⌃q)<latexit sha1_base64="hv19xxln5Ihgt0PDz00mX3beYGs=">AAACF3icbZC7TsMwFIadcivlVmCEwaJCKkuVICQYq8LAWBC9SE1UOY7TWnXsYDtAFXXhLXgDVngBNsTKyM6D4LYZoOVIln79/znH9ufHjCpt219WbmFxaXklv1pYW9/Y3Cpu7zSVSCQmDSyYkG0fKcIoJw1NNSPtWBIU+Yy0/MH5OG/dEamo4Dd6GBMvQj1OQ4qRNla3uO/WxEM5dq9pr6+RlOLevaAoEjyAt0fdYsmu2JOC88LJRAlkVe8Wv91A4CQiXGOGlOo4dqy9FElNMSOjgpsoEiM8QD3SMZKjiCgvnfxiBA+NE8BQSHO4hhP390SKIqWGkW86I6T7ajYbm/9lnUSHZ15KeZxowvH0ojBhUAs4RgIDKgnWbGgEwpKat0LcRxJhbcAV3PHCDGHqCxaMDBZnFsK8aB5XHLviXJ2UqrUMUB7sgQNQBg44BVVwCeqgATB4BM/gBbxaT9ab9W59TFtzVjazC/6U9fkDl7ugSA==</latexit>

FormalMethods

ColControl
Theorylabo

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>

rationProblem: scalability, esp. for real-world CPSs
Require complete understanding of a white-box model
Insist on being absolutely sound and correct
Little tolerance to uncertainty and noise➜ don’t get along with statistical machine learning

5

CPS Research:
Our Comprehensive Approach
Control Theory

Formal Methods

6

CPS Research:
Our Comprehensive Approach
Control Theory

Formal Methods

Statistical
MachineLearning

SoftwareEngineering
6

CPS Research:
Our Comprehensive Approach
Control Theory

Mathematical
Metatheory

Formal Methods

StatisticalMachine
Learning

SoftwareEngineering
6Bidirectional Collaboration withStatistical Machine LearningStatisticalML

Inductive(learn from data)

Uncertainty(data is noisy)(Typically)
Black Box

FormalMethods,
Control Th.

Deductive

Mathematical &Logical Rigor

White Box

(Infer from absoluteaxioms)

7

Bidirectional Collaboration with
Statistical Machine Learning
StatisticalML

Inductive(learn from data)

Uncertainty(data is noisy)(Typically)
Black Box

FormalMethods,
Control Th.

Deductive

Mathematical &Logical Rigor

White Box

(Infer from absoluteaxioms)

StatisticalML

Formal Methods
Control Theory

7

Bidirectional Collaboration with
Statistical Machine Learning
StatisticalML

Inductive(learn from data)

Uncertainty(data is noisy)(Typically)
Black Box

FormalMethods,
Control Th.

Deductive

Mathematical &Logical Rigor

White Box

(Infer from absoluteaxioms)

StatisticalML

Formal Methods
Control Theory

7

Bidirectional Collaboration with
Statistical Machine Learning
StatisticalML

Inductive(learn from data)

Uncertainty(data is noisy)(Typically)
Black Box

FormalMethods,
Control Th.

Deductive

Mathematical &Logical Rigor

White Box

(Infer from absoluteaxioms)
Accelerate search/
constraint solving/
optimization

StatisticalML

Formal Methods
Control Theory

7

Bidirectional Collaboration with
Statistical Machine Learning
StatisticalML

Inductive(learn from data)

Uncertainty(data is noisy)(Typically)
Black Box

FormalMethods,
Control Th.

Deductive

Mathematical &Logical Rigor

White Box

(Infer from absoluteaxioms)
Accelerate search/
constraint solving/
optimization

StatisticalML

Formal Methods
Control Theory
Acknowledge that ML
components are unreliable
Wrap them with “safetyenvelopes,”within which ML optimizes
7[Akametalu, Kaynama,Fisac, Zeilinger, Gillula& Tomlin, CDCʼ14]

Key: system-level architecture forcollaboration between logic and ML.
Separation of concernsBidirectional Collaboration with
Statistical Machine Learning
StatisticalML

Inductive(learn from data)

Uncertainty(data is noisy)(Typically)
Black Box

FormalMethods,
Control Th.

Deductive

Mathematical &Logical Rigor

White Box

(Infer from absoluteaxioms)
Accelerate search/
constraint solving/
optimization

StatisticalML

Formal Methods
Control Theory
Acknowledge that MLcomponents are unreliable
Wrap them with “safetyenvelopes,”within which ML optimizes
7[Akametalu, Kaynama,
Fisac, Zeilinger, Gillula& Tomlin, CDCʼ14]

Challenges in industrial application
Scalability: real systems are complexhttp://www.popularmechanics.com/cars/how-to/
a7386/how-it-works-the-computer-inside-your-car/

Software Engineering and Empirical Applicationof Formal Methods and Control Theory
Need complete white-box models
Unrealistic. Components from suppliers, neural nets, …
Industry practitioners need not appreciate rigorous proofs
How do we check axioms (= environmental assumptions)?

8?

Challenges in industrial application
Scalability: real systems are complex

http://www.popularmechanics.com/cars/how-to/
a7386/how-it-works-the-computer-inside-your-car/

Software Engineering and Empirical Applicationof Formal Methods and Control Theory
Need complete white-box models
Unrealistic. Components from suppliers, neural nets, …
Industry practitioners need not appreciate rigorous proofs
How do we check axioms (= environmental assumptions)?
➜ We focus on supporting empirical quality assurance methods(i.e. testing)
What software engineering has been doing for years
Testing, runtime verification, …
Ample use of deductive techniques from formal methods
Examples: from specifications to score functions,
optimize test cases, …
Talks by Etienne Andre, Masaki Waga, Paolo Arcaini
8?

Exit Strategy(in Application)
Outlets
Industry collaboration: a few companies
Automated Driving Vehicle Project “Autonomoose” (U Waterloo).
(Mostly) nonproprietary software stack for automated driving

9

Exit Strategy(in Application)
Outlets
Industry collaboration: a few companies
Automated Driving Vehicle Project “Autonomoose” (U Waterloo).
(Mostly) nonproprietary software stack for automated driving

9

Exit Strategy(in Application)
Outlets
Industry collaboration: a few companies
Automated Driving Vehicle Project “Autonomoose” (U Waterloo).
(Mostly) nonproprietary software stack for automated driving
Goal 1: our advanced quality assurance techniques, put to real use
Safety is rarely a competition area
➜ we aim at standards (ISO 26262, SOTIF, …)

9Exit Strategy(in Application)
Outlets
Industry collaboration: a few companies
Automated Driving Vehicle Project “Autonomoose” (U Waterloo).
(Mostly) nonproprietary software stack for automated driving
Goal 1: our advanced quality assurance techniques, put to real use
Safety is rarely a competition area
➜ we aim at standards (ISO 26262, SOTIF, …)
Goal 2: offer software platform fordeveloping, verifying and validating automated driving software
For industry and academia
Perception ➜ Object Recognition ➜ Path Planning ➜ Path Tracing,+ Simulation + Testing, V&V
我々の貢献領域
Strategic contribution areas
Improvement of each component＋ Interface between components, DSL (domain specific language)➜ the whole framework
Our unique strength: advanced V&V techniques + their theoretical foundation +programming language theory
9

CPS Research:
Our Comprehensive Approach
Mathematical metatheory
Control Theory

Formal Methods

Statistical
MachineLearning

SoftwareEngineering
10

CPS Research:
Our Comprehensive Approach
Mathematical metatheory
Control TheoryEtienne Andre
Masaki Waga
Akihisa Yamada
Kenta Cho

Formal Methods

Clovis Eberhart
Natsuki Urabe
Toru Takisaka

Statistical
MachineLearning

SoftwareEngineering
10

Chao Huang
Paolo Arcaini

CPS Research:
Our Comprehensive Approach
abstraction

Mathematical metatheory
Control Theory

Etienne Andre
Masaki Waga
Akihisa Yamada
Kenta Cho

Formal Methods

Clovis Eberhart
Natsuki Urabe
Toru Takisaka

Statistical
MachineLearning

SoftwareEngineering
10

Chao Huang
Paolo Arcaini

CPS Research:
Our Comprehensive Approach
abstraction

Mathematical metatheory
Control Theory

Etienne Andre
Masaki Waga
Akihisa Yamada
Kenta Cho

Formal Methods

Clovis Eberhart
Natsuki Urabe
Toru Takisaka

StatisticalMachine
Learning

SoftwareEngineering
10

Chao Huang
Paolo Arcaini