Formal Methods for
Cyber-Physical Systems, at Work

Ichiro Hasuo
National Institute of Informatics & SOKENDAI
Research Director, ERATO MMSD Project, JSTOutline
Quality assurance of cyber-physical systems
Formal methods at work,
coping with uncertainties
Introducing the ERATO MMSD project
Tech showcase:“formal methods that are down-scalable”
Monitoring
Search-based testing
Applications, “power of math”
2

Hasuo (NII, Tokyo)

Cyber-Physical Systems：
Control Theory and Formal Methods/Software Science
Cyber-Physical System(CPS)“A mechanism that is controlled ormonitored by computer-basedalgorithms, tightly integrated with theInternet and its users” (Wikipedia)

Physical plant(continuous)+
Digital control (discrete)
In US: NSF Key Area ofResearch (2006-)
3

Cyber-Physical Systems：
Control Theory and Formal Methods/Software Science
Formal methods:
Logical proofs for “correctness” of(discrete) programs
Model checking(SPIN, NuSMV, Uppaal, PRISM, …) [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 recognizede.g. HSCC, one of the main
conferences ofannual CPS Week
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

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

rati
on

Problem: practical applicability. Why?
Scalability
Uncertainties.
Physical environments, black-box models, statistical AI/ML, …

5

On ERATO MMSDJST ERATO Project, 2016/10-2022/03
https://group-mmm.org/eratommsd
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”
Emphasizing industry collaboration, also forscientific inspirations
Automated driving as a strategic target domain.
Collaboration with U Waterloo:
www.autonomoose.net
Our team:
28 researchers, > 20 students (as of 2019/09)
International and scientifically diverse
6

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
Subleader: Paolo Arcaini
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)

Members

G02019.6, Tokyo NII Site

G1

G3Group Leaders,
Assoc. Profʼs
Shin-ya
KatsumataIchiroHasuo

MasakoKishidaEtienneAndre

FuyukiIshikawa

Paolo
Arcaini

Assistant Profʼs(and similar)
JeremyDubut

TaroSekiyama

Akihisa
YamadaAhmet
Cetinkaya

Tsutomu
Kobayashi

Chao
Huang

Xiaoyi
Zhang

Post-docs(and similar)David
SprungerClovisEberhart

Kenta
Cho

Sasinee
Pruekprasert

Toru
Takisaka

Grad Students,
RAs
Satoshi
Kura

Yuichi
Komorida

Takamasa
Okudono8

Sang-Hwa
Lee

Liye
Guo

Masaki
Waga

ZhenyaZhang

- Top researchers from theMembers

world, selected out of > 150
applications
G0
2019.6,
Tokyo NII Site

FR

IT

G1

G3

Group Leaders,
Assoc. Profʼs
Shin-ya
Katsumata

TUR(PhD,Masako
TokyoTech) Etienne

IchiroHasuo

KishidaFuyukiIshikawa

Andre

Paolo
Arcaini

FR

Assistant Profʼs(and similar)
US

FR

JeremyDubut

TH(PhD, Osaka)David
SprungerClovisEberhart

Kenta
Cho

Taro
Sekiyama

Akihisa
Ahmet
CN
YamadaCetinkaya

CN

Tsutomu
Kobayashi

Post-docs(and similar)
SasineeKR
Pruekprasert

Toru

CN
Takisaka

Chao
Huang

Xiaoyi

CNZhang

Grad Students,
RAs
Satoshi
Kura

Yuichi
Komorida

Takamasa
Okudono9

Sang-Hwa
Lee

Liye
Guo

Masaki
Waga

ZhenyaZhang

Interdisciplinary Efforts towards CPS:
Six Scientific Fields
application

Cyber-Physical Systems(esp. Automated Driving)F

Statistical ML & AI

Software Science
Formal Methods

D

BE

Control
Theoryfoundation

SoftwareEngineeringC(Meta-)Theoretical
Foundation
10

A• Four academic fields (B,C,D,E)
closely collaborating,• driven by clear application goals(F), and• backed up by mathematicalfoundation (A)Academic Achievements
International visibility:
CORE rank A* (top 4%, LICS, CAV, POPL, …):> 10 papers
CORE rank A (top 5~18%, ATVA, TACAS, GECCO, ICECCS, …):> 20 papers
Best paper awards：
ICECCS’18, FoSSaCS’19 (CORE rank A), FORMATS’19
At LICS’19 (CORE rank A*):
6 out of 60 accepted papers were coauthored by us

11

Hasuo (NII, Tokyo)

Outline
Quality assurance of cyber-physical systems
Formal methods at work,
coping with uncertainties
Introducing the ERATO MMSD project
Tech showcase:“formal methods that are down-scalable”
Monitoring
Search-based testing
Applications, “power of math”
12

Hasuo (NII, Tokyo)

Confidential

Pattern Matching against Timed Automata,
Monitoring
Specification“Frequent gear changes within 3 sec after shifting up to 4th”

60
45
30
15
0

Runningsystem

0

10

20

30

Log

Monitor

Runtime verification, monitoring
Not straightforward, esp. when specs involve timing constraints
Speed requirements (GBs of log per second)
Computing resource (embedded)…
Industry needs
Technically: theory of (parametrized) timed automata

Monitoring
result“From 18.9 sec. to
23.2 sec.”

Pattern Matching against Timed Automata,
Monitoring
Specification“Frequent gear changes within 3 sec after shifting up to 4th”

60
45
30
15
0

Runningsystem

0

10

Log

20

30

MonitorMonitoring
result“From 18.9 sec. to
23.2 sec.”

Use cases“Here is 1 PB of log, and I want to extract its relevant parts”“Raise an alert if this specific type of anomaly occurs”

Monitoring: Problem Formulations
Given: a log, discrete time w = abaaacb…bbc
a spec φ”no occurrence of c for 6 steps after b”
Answer: all subsequences of w that satisfy φNontrivial due to temporalcausality

Given: a log, continuous time w = (a, 0.12) (b, 1.28) …
a spec φ ”no occurrence of c for 6 seconds after b”
Answer: all subsequences of w that satisfy φ[Ulus, CAV’17] [Waga+, FORMATS’17]

Infinitely many such subsequences(starting at t=1? t = 1.01? t = 1.001? …)➜ Efficient representation & computation by zones

Given: a log, continuous time w = (a, 0.12) (b, 1.28) …
a parametrized spec φ(p)”no occurrence of c for p seconds after b” “b occurs with a period of p seconds”

Answer: all the pairs of (p, (a subseq. of w that satisfies φ)))[Andre+, ICECCS’18] [Waga+, NFM’19] [Waga+, CAV’19] …

In industry, fixing a spec is a big challenge.
Parameters ➜ flexibility in specs
15
Hasuo (NII, Tokyo)

Monitoring: Our Achievements
Efficient algorithm from
Given: a log, discrete time w = abaaacb…bbc
theory of timed automata.
a spec φ”no occurrence of c for 6 steps after b” Processes ~ 1M events/
second (laptop).
Answer: all subsequences of w that satisfy φ[Waga+, FORMATS’17]

Given: a log, continuous time w = (a, 0.12) (b, 1.28) …
a spec φ ”no occurrence of c for 6 seconds after b”
Answer: all subsequences of w that satisfy φ[Ulus, CAV’17] [Waga+, FORMATS’17]

https://github.com/maswag/monaa

Also implemented onRenesas RH850

Efficient algorithm using parametrized timed automata.
Processes ~ 10K events/second (laptop). [Waga+, NFM’19]
https://github.com/maswag/symon

Given: a log, continuous time w = (a, 0.12) (b, 1.28) …
a parametrized spec φ(p)”no occurrence of c for p seconds after b” “b occurs with a period of p seconds”

Answer: all the pairs of (p, (a subseq. of w that satisfies φ)))[Andre+, ICECCS’18] [Waga+, NFM’19] [Waga+, CAV’19] …
16

Hasuo (NII, Tokyo)

Search-Based
Testing by Reinforcement Learning[Zhang+, EMSOFT’18] [Zhang+, CAV’19] [Fainekos & Pappas, TCS’09]

Black-box, search-based testing. Actively search for erroneous input by:
Try an input
signalObserve thesystem’s behavior

throttle

speed
60
45
30
15
0

time
brake

Choose the next
input that is likely
to be erroneous

0

10

20

30

10

20

30

RPM
70
52.5
35
17.5
0

time

[Fainekos & Pappas, TCS’09]
A reinforcement learning problem,by moving

more robustly
true

??

true

from the Boolean semantics(erroneous or not)

false

input

Boolean semantics

to quantitative “robust semantics”(how far from being erroneous)
170This way toclimb down :)less soquantitativerobust semantics

inputSearch-Based Testing byReinforcement Learning[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 verification of embedded control systems: An overview of traditional
and advanced modeling, testing, and verification techniques,” IEEE Control Syst., vol. 36, no. 6, pp. 45–64, Dec. 2016.

Our Contribution In [Zhang+, EMSOFT’18] [Zhang+, CAV’19]
Exploit discrete structures in stochastic gradient descent➜ efficient and extensive search➜ interpretable testingMonte-Carlo Tree Search

In the form of hierarchical optimization

Discrete Optim.
Feed search
results backFocus
searchdomain

Domainsequence for
guidingsearchContinuous Optim.
Stochastic gradient descent(simulated annealing, CMA-ES, …)
18

Towards Formal Methods That Are
Down-Scalable
Many FM methods are not down-scalable
They demand white-box models

degree ofguarantee

Mathematical
proofs,strong guarantee➜ huge cost before non-zero benefit
Example applications to CPS:
airplanes (Airbus), space (NASA), …
Failure is so expensive➜ worth verification effots

cost
Costly to constructwhite-box models

Still takes decades
Integrating continuous dynamics is hard
➜ They focus on software

19

Towards Formal Methods That Are
Down-Scalable
Real-world applications(esp. automotive domain),need down-scalability

degree ofguarantee

Even if we can only afford
half the cost,degree of guarantee does not
become zero, but half✘✔

Our efforts at ERATO MMSD
Combinetesting and formal verification.
Search-based testing, monitoring

cost

Contract-based verification➜ formal safety architecture(contract-based verification, see
reserve slides)
20

Hasuo (NII, Tokyo)

Outline
Quality assurance of cyber-physical systems
Formal methods at work,
coping with uncertainties
Introducing the ERATO MMSD project
Tech showcase:“formal methods that are down-scalable”
Monitoring
Search-based testing
Applications, “power of math”
21

Hasuo (NII, Tokyo)

Industry Collaboration
Mainly automotive,
but not exclusively
Production systems
AI startups
Inspiring scientific research, too
New problems
Solve a problem➜ generalize the solution➜ scientific novelty
A lot of industry needs
Methods applicableoﬀ-the-shelf(monitoring, search-based testing)High demand forformal verification“What is an expected level ofquality assurance?”
22

Hasuo (NII, Tokyo)

Collaboration with U Waterloo
test tool

perception

object recognition

local planningbehavior planning

path tracking

path planning

env. input(road shape,
pedestrians,
other cars, …)

ego carʼs
position & status
Our goal: comprehensive software stackwith perception units, controllers,simulators, and testing tools（cf. ROS, robot operating system）- serving academic users- used as (part of) prototype products- testbed for technical components

Simulation environment
23

Hasuo (NII, Tokyo)

24Traced monoidal categories

logic, algebra,
category theory,✓◆
theory of coalgebras…
Defn. T (e) =, where Be is a monadin K`(Be )Abstract TechniqueThm. Coalgebraic proof methods (such as (bi)simulations) are v
A

T[_][Sprunger & Katsumata, LICS’19]

Proof.

::=

true | false | A1 ^ A2 | ¬A | a1 < a2 |8x 2 ⇤N. A | 8x 2 ⇤R. A

By the following characterizations in K`(Be ).
FX
O
c
X

F behc /

F OZ
final
/Z

behc
system behavior

Identify“mathematicalessense”

Chooseparameter e1

Existing Technique

Reachability in
Automata

Ff
w

/ FY
O
d
/Y

f
simulation

Chooseparameter e2
Novel Technique

T1 = T[e1]knot invariants, QFTs,
semantics of recursion, …

FX
O
c
X

T[e2]
back-propagation algorithm
for recurrent neural networks
Reachability probabilities inprobabilistic
Result automata
that stemmed from“deep learning reading group” at ERATO MMSD
25

Power of MathContribution of “theoreticians and listeners” have beenremarkable, direct and indirect“Metatheoretical transfer”
Interpreters between disciplines
Great “reserve forces”
26

Hasuo (NII, Tokyo)

Conclusions
Quality assurance of cyber-physical systems
Formal methods at work,
coping with uncertainties
Introducing the ERATO MMSD project
Tech showcase:“formal methods that are down-scalable”
Monitoring

ion!
t
n
e
t
t
a
r
u
o
y
r
Thanks fo
sd
m
m
o
t
a
r
e
/
g
r
.o
mmm
p
u
o
r
g
/
/
:
s
p
t
t
h

Search-based testing

Applications, “power of math”
27

Hasuo (NII, Tokyo)

Reserve Slides

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 a
Example: simplex
architecture(right)challenging
problem thatyields significant benefits. By utilizing
A-G contracts, we are able to compositionally determine theAC isswitching logic for CBSAs, thereby alleviating the state explosion
encountered by other approaches. black-box
Another benefit is that wecomplex, performance-oriented,
can use A-G proof rules to decompose the proof of system-widesafety assurance into sub-proofs corresponding to the componentBC isbased structure of the system architecture. We also introduce thesimple, safety-oriented,
notion of coordinated (hopefully)
switching betweenwhite-box
Simplex instances, a key
component of our compositional approach to reasoning about
CBSA switching logic.
Idea: we can verify
wholesystemwith a component-based control
Wethe
illustrate
our frameworksystem for a ground rover. We formally prove that the CBSA foreven if AC is a black-box!
this system guarantees energy safety (the rover never runs outof power), and collision freedom (the rover never collides with
Enough to show:
a stationary obstacle). We also consider a CBSA for the roverthat andguarantees
mission completion:
all target destinations visited
safety of BC,
correctnessof DM
within a prescribed amount of time.
Index Terms—Simplex
architecture;
We impose certain
contracts
on AC 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.

Formal Safety 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 ofRelatedthis form is illustrated in Fig. 2. Furthermore, some of theseI. I NTRODUCTION
controllers themselves may have a hierarchical or nested
FM4AI (ML/AI
components
asAC)
Simplex [1]–[3] is a software architecture for high-assurance structure.
Advanced control systems are not necessarily hierarchical,
It traditionally
Monitoringprocess-control(checking systems.
contracts
on AC)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
One promising way
to of the plant under nominal operating conditions, distinguished physical-plant node (we do not consider multiple
in control
make formal verification
down-scalable
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
Weaker contracts
on AC
completion time). The BC is pre-certified to keep the plant for component-based control systems that are equally modular,➜ weaker safety
guarantee
hopefully
within a prescribedsafety(butregion,i.e., a regionnon-zero)of safe op- to reduce their associated complexity and cost.
eration. A decision module (DM), which is also pre-certified,Components may have different update periods (or excontinually monitors the state of the plant and 29
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 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[Abrial,component“The Event-B
2010 approach
CUP] [Kobayashi+,of our Book”,
compositional
to reasoning about
CBSA switching logic.
ICFEM’18]
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.

Formal Safety Architecture
At ERATO MMSD:
we formalize, verify and refine
safety architectures

Event-B: a formal modeling language
Based on state transition systems.
A tool Rodin supports:

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 have
Safety proofsa hierarchical control system consisting of controllers for (inorder of decreasing level of abstraction) mission-planning,
Incremental modeling by refinements
guidance, navigation, and inner-loop control. A system ofthis form is illustrated in Fig. 2. Furthermore, some of these
FlexibilityI. Iinchoosing
model
NTRODUCTION
controllers themselves may have a hierarchical or nested
fidelity
down-scaling
Simplex[1]–[3] is➜a softwarearchitecture for high-assurance structure.
Advanced control systems are not necessarily hierarchical,
process-control systems. It traditionally consists of a physFrom(our)generalmodel
tobut are better understood as having a component-based arical plant
and twoversionsof the controller:
an advanced
controller(AC) and a partner’s)baseline controllerindividual(BC). The AC is chitecture. A “component” may be a software module or the(industryin control of the plant under nominal operating conditions, distinguished physical-plant node (we do not consider multiple
and ismodel
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
30completion time). The BC is pre-certified to keep the plant for component-based control systems that are equally modular,