Falsification of Cyber-Physical
Systems with RobustnessGuided Black-Box Checking
Masaki Waga1,2,3
National Institute of Informatics1, SOKENDAI2,JSPS Research Fellow3
April 2020, HSCC 2020
This work is partially supported by JST ERATO HASUO Metamathematics for Systems
Design Project (No. JPMJER1603), by JSPS Grants-in-Aid No. 15KT0012 & 18J22498

1

M. Waga (NII)Testing is Important…

https://www.bbc.com/news/technology-48308852
https://www.qfs.de/fr/blog/article/2019/07/11/utiliser-qf-test-dans-des-systemes-continuous-integration-1.html

2M. Waga (NII)Testing is Important…

https://www.bbc.com/news/technology-48308852
https://www.qfs.de/fr/blog/article/2019/07/11/utiliser-qf-test-dans-des-systemes-continuous-integration-1.html

2

M. Waga (NII)

Falsification: Robustness + Optimization
ℳ

ℳ(σ)

σσ

Robustness Monitor
Spec:
in−STL
ρ(ℳ(σ),
φ) φ=φ)ρ(ℳ(σ),=1030(signal temporal logic)

Optimizer(Minimize Robustness)

3

M. Waga (NII)

Falsification: Robustness + Optimization
ℳ

σℳ(σ)

σ

Robustness Monitor
Spec:
in−STL
ρ(ℳ(σ),
φ) φ=φ)ρ(ℳ(σ),=1030(signal temporal logic)

Optimizer(Minimize Robustness)

3

M. Waga (NII)

Falsification: Robustness + Optimization
ℳℳ(σ)

σℳ(σ)
σ

σ

Robustness Monitor
Spec:in−STL
ρ(ℳ(σ),
φ) φ=φ)ρ(ℳ(σ),=1030(signal temporal logic)

Optimizer(Minimize Robustness)

3

M. Waga (NII)

Falsification: Robustness + Optimization
ℳ

ℳ(σ)

σ
ℳ(σ)
σ

ℳ(σ)

σ

Robustness MonitorSpec:ρ(ℳ(σ),
φ) φ=in−STL
10(signal temporal logic)

Optimizer(Minimize Robustness)ρ(ℳ(σ), φ) = 30
3

M. Waga (NII)

Falsification: Robustness + Optimizationℳℳ(σ)σσℳ(σ)σℳ(σ)

Robustness MonitorSpec:ρ(ℳ(σ),
φ) φ=in−STL10(signal temporal logic)

Optimizer
ρ(ℳ(σ), φ) = 30(Minimize Robustness)ρ(ℳ(σ), φ) = 30
3

M. Waga (NII)

Falsification: Robustness + Optimization
ℳℳ(σ)

σσσ

ℳ(σ)

ℳ(σ)

Robustness Monitor
Spec: φ in STL(signal temporal logic)

Optimizer
ρ(ℳ(σ), φ) = 30
(Minimize Robustness)✘ρ(ℳ(σ), φ) = 30
ρ(ℳ(σ), φ) = − 103

M. Waga (NII)Robustness of STL
Booleanx100⊧ □ x > 10⊧ □ x > 10x
5/⊧ □ x > 10x-60, □ x > 10) = 90(xρ 100xx
15Robust/⊧ □ x > 10

ρ(15, □ x > 10) = 5x, □ x > 10) = -5

ρ( 5ρ(x, □ x > 10) = -70-60

4Clearlysatisfied

Boarder
Clearly
violated

M. Waga (NII)σFalsificationisOneshotℳℳ(σ)

Spec. 1
Optimizer(Minimize Robustness)σρ(φ1, σ) = 30ℳ

Robustness Monitor
Spec: φ1ℳ(σ)

Spec. 2
Optimizer(Minimize Robustness)

Robustness Monitor
ρ(φ2, σ) = 75
Spec: φ2
M. Waga (NII)
5σ

FalsificationisOneshotℳℳ(σ)

Spec. 1Optimizer(Minimize Robustness)σρ(φ1, σ) = 30ℳ

Robustness Monitor
Spec: φ1ℳ(σ)

tnednepedIn.
ofnIdesue→ No R

Spec. 2
Optimizer(Minimize Robustness)

Robustness Monitor
ρ(φ2, σ) = 75
Spec: φ2
M. Waga (NII)
5

Falsification is Oneshot
σ

ℳℳ(σ)

Version 1
Optimizer(Minimize Robustness)σρ(φ, σ) = 30ℳ

Robustness Monitor
Spec: φℳ(σ)

Version 2
Optimizer(Minimize Robustness)ρ(φ, σ) = 75
6Robustness Monitor
Spec: φM. Waga (NII)

Falsification is Oneshotσℳℳ(σ)

Version 1
Optimizer(Minimize Robustness)σρ(φ, σ) = 30

Robustness Monitor
Spec: φtnednepedIn.
ofnIdesue→ No Rℳℳ(σ)

Version 2
Optimizer(Minimize Robustness)ρ(φ, σ) = 75
6Robustness Monitor
Spec: φM. Waga (NII)Q. How to reuse the previous
exploration information

7

M. Waga (NII)Q. How to reuse the previous
exploration information

Our Approach:Black-Box Checking (BBC)7

M. Waga (NII)Black-Box Checking (BBC)[Peled+, FORTE’99]~Learn Autom. ℳ
from CPS ℳ
Model Check~ℳ⊧φ?
No

No. cex u

NoYes~ℳ≈ℳℳ(u) /⊧ φ
Yes~

✘8Yes

✓
M. Waga (NII)Black-Box Checking (BBC)[Peled+, FORTE’99]~

Learn Autom. ℳ Approximate ℳ~ℳ.
motfrom CPS ℳ
uayb
Model Check~ℳ⊧φ?
No

No. cex uℳ(u) /⊧ φ~

Exploit ℳ
No

Yes

~

Validate ℳ

Yes~

✘8~

ℳ≈ℳ
Yes

✓
M. Waga (NII)Black-Box Checking (BBC)[Peled+, FORTE’99]~

Learn Autom. ℳ Approximate ℳ~ℳ.
motfrom CPS ℳ
uayb
Model Check~ℳ⊧φ?
No

No. cex uℳ(u) /⊧ φ
Yes~
✘ +ℳ

~

Exploit ℳ
NoYes~

Validate ℳ~
Reuse ℳ
8~

ℳ≈ℳ
Yes~+
✓ ℳ

M. Waga (NII)Black-Box Checking (BBC)[Peled+, FORTE’99]~

Learn Autom. ℳ Approximate ℳ~ℳ.
motfrom CPS ℳ
uayb
Model Check~ℳ⊧φ?
NoNo. cex uℳ(u) /⊧ φ
Yes~
✘ +ℳ

~

Exploit ℳ
No

Yes~Validate ℳ~
Reuse ℳ
8~ℳ≈ℳ

DiﬃcultYes~+✓ ℳ

M. Waga (NII)~

Equivalence Test: ℳ ≈ ℳ•

Theoretically: Automata-based conformance teste.g., W-method [Chow, TSE’78], Wp-method [Fujiwara+, TSE’91]••☹ # of states is necessary for soundness

Practically:•Random test
• ☹ Not good at “rare” cex

9M. Waga (NII)~Equivalence Test: ℳ ≈ ℳ•

Theoretically: Automata-based conformance test
e.g., W-method [Chow, TSE’78], Wp-method [Fujiwara+, TSE’91]••☹ # of states is necessary for soundness

Practically:•Random test
• ☹ Not good at “rare” cex

Q. How about hitting “rare” cexwith robustness of STL?
9M. Waga (NII)Robustness-Guided Equivalence Test
[Contribution]••

Equivalence Test with Robustness + Optimization~• Search for u s.t. ℳ(u) ≠ ℳ(u)•Genetic algorithm or hill climbing•

Fitness function: Robustness of STL~

ℳ is not directly evaluated•~Discrete behavior of ℳ is not a problem
Detail is later
10M. Waga (NII)

Contributions•

Presented robustness-guided equivalence test•

Also introduced a new robustness suitable tomodel checking•

Used it for black-box checking of CPS•

Experimental evaluation: outperforms the baseline

11

M. Waga (NII)Outline•

Introduction•

Preliminary: Black-box checking••Main Contribution:Robustness-guided equivalence test••

Automata learning, model checking, & equiv. test

idea: Optimization + robustness

Experiments
12M. Waga (NII)Black-Box Checking (BBC)[Peled+, FORTE’99]~

Learn Autom. ℳ
from CPS ℳ

ℳ
et
am
i
xor
p
Ap
~
by autom. ℳ
NoNo
Model Check~ℳ⊧φ?
No. cex u~✘ +ℳ

Exploit ℳ
Yes~

ℳ≈ℳ

ℳ(u) /⊧ φYes~~

Validate ℳ
13Yes~+✓ ℳ

M. Waga (NII)Black-Box Checking (BBC)[Peled+, FORTE’99]~

Learn Autom. ℳ
from CPS ℳℳetamixorpAp~
by autom. ℳ
NoNoModel Check~ℳ⊧φ?
No. cex u~✘ +ℳ

Exploit ℳYes~ℳ≈ℳℳ(u) /⊧ φYes~~Validate ℳ
13Yes~+✓ ℳ

M. Waga (NII)

Automata Learning
1. Obtain suitable input/output pairs (u, ℳ(u)) of ℳ•

Input/output: finitely discretized

2. Generate a candidate Myhill-Nerode equiv. rel.
~

3. Construct the corresponding Mealy machine ℳ

14

M. Waga (NII)Black-Box Checking (BBC)[Peled+, FORTE’99]~Learn Autom. ℳ
from CPS ℳℳ
etamixorp
Ap~by autom. ℳ
NoNo
Model Check~ℳ⊧φ?
No. cex u~✘ +ℳ

Exploit ℳ
Yes~

ℳ≈ℳ

ℳ(u) /⊧ φYes~~

Validate ℳ
15Yes~+✓ ℳ

M. Waga (NII)Black-Box Checking (BBC)[Peled+, FORTE’99]~

Learn Autom. ℳ
from CPS ℳℳ
etamixorp
Ap~by autom. ℳ
NoNo
Model Check~ℳ⊧φ?
No. cex u~✘ +ℳ

Exploit ℳ
Yes~

ℳ≈ℳ

ℳ(u) /⊧ φYes~~

Validate ℳ
15Yes~+✓ ℳ

M. Waga (NII)~

Model Check: ℳ ⊧ φ ?
Issue: φ is not in LTL but in STL
Our Solution: Encode to LTL model checking
STLφ ::= x ⋈ c ∣ φ ∧ φ ∣ ⋯ ∣ φ𝒰I φLTLφ ::= P ∣ φ ∧ φ ∣ ⋯ ∣ φ𝒰φ

Inequality

Proposition

Assumption:
signal is discrete-time with constant interval
16

M. Waga (NII)Black-Box Checking (BBC)[Peled+, FORTE’99]~

Learn Autom. ℳ
from CPS ℳ

ℳ
etami
xor
p
Ap~
by autom. ℳ
NoNo
Model Check~ℳ⊧φ?
No. cex u~✘ +ℳ

Exploit ℳ
Yes~

ℳ≈ℳ

ℳ(u) /⊧ φYes~~

Validate ℳ17Yes~✔ +ℳ

M. Waga (NII)Black-Box Checking (BBC)[Peled+, FORTE’99]~

Learn Autom. ℳ
from CPS ℳℳetamixorp
Ap~by autom. ℳ
NoNo
Model Check~ℳ⊧φ?
No. cex u~ℳ(u) /⊧ φ
Yes~
✘ +ℳ

~

Exploit ℳ
Yesℳ(u) /⊧ φ~ℳ≈ℳ~

Validate ℳ
17

Yes~
✔ +ℳ

M. Waga (NII)Black-Box Checking (BBC)[Peled+, FORTE’99]~

Learn Autom. ℳ
from CPS ℳℳ
etamixorp
Ap~by autom. ℳ
NoNo
Model Check~ℳ⊧φ?
No. cex u~ℳ(u) /⊧ φYes~✘ +ℳ~

Exploit ℳ
Yesℳ(u) /⊧ φ~ℳ≈ℳ~

Validate ℳ
17Yes~✔ +ℳ

M. Waga (NII)Black-Box Checking (BBC)[Peled+, FORTE’99]~

Learn Autom. ℳ
from CPS ℳℳ
etamixorpAp~
by autom. ℳ
NoNo
Model Check~ℳ⊧φ?
No. cex u~ℳ(u) /⊧ φ
Yes~
✘ +ℳ

~

Exploit ℳ
Yesℳ(u) /⊧ φ~ℳ≈ℳ

Simulation~
Validate ℳ
17Yes~✔ +ℳ

M. Waga (NII)Black-Box Checking (BBC)[Peled+, FORTE’99]~

Learn Autom. ℳ
from CPS ℳℳ
etamixorpAp~
by autom. ℳ
NoNo
Model Check~ℳ⊧φ?
No. cex u~ℳ(u) /⊧ φ
Yes~
✘ +ℳ

~

Exploit ℳ
Yesℳ(u) /⊧ φ~ℳ≈ℳ~

Validate ℳ
18

Yes~
✔ +ℳ

M. Waga (NII)Black-Box Checking (BBC)[Peled+, FORTE’99]~

Learn Autom. ℳ
from CPS ℳℳ
etamixorpAp~
by autom. ℳ
NoNo
Model Check~ℳ⊧φ?
No. cex u~ℳ(u) /⊧ φ
Yes~
✘ +ℳ

~

Exploit ℳ
Yesℳ(u) /⊧ φ~ℳ≈ℳ~

Validate ℳ
18

Yes~
✔ +ℳ

M. Waga (NII)Black-Box Checking (BBC)[Peled+, FORTE’99]~

Learn Autom. ℳ
from CPS ℳℳ
etamixorp
Ap~by autom. ℳ
NoNoModel Check~ℳ⊧φ?
No. cex u~ℳ(u) /⊧ φ
Yes~
✘ +ℳ~

Exploit ℳ
Yesℳ(u) /⊧ φ~ℳ≈ℳ~

Validate ℳ
18DiﬃcultYes~✔ +ℳ

M. Waga (NII)Outline•

Introduction•

Preliminary: Black-box checking••

Main Contribution:
Robustness-guided equivalence test••

Automata learning, model checking, & equiv. test

idea: Optimization + robustnessExperiments
19M. Waga (NII)Robustness-Guided Equivalence Test[Contribution]

Gen. population U

U := U'~∀u ∈ U . ℳ(u) = ℳ(u) ?

NoReturn u

YesGen. next population U'

Selection: u' ∈ U' s.t.

ρ(ℳ(u′), φ) is small
20

M. Waga (NII)Robustness-Guided Equivalence Test
[Contribution]

Gen. population U

U := U'~∀u ∈ U . ℳ(u) = ℳ(u) ?

NoReturn u

YesGen. next population U'

Selection: u' ∈ U' s.t.

ρ(ℳ(u′), φ) is small
20

M. Waga (NII)Robustness-Guided Equivalence Test
[Contribution]

Gen. population UU := U'~∀u ∈ U . ℳ(u) = ℳ(u) ?
YesGen. next population U'No

Return u&revossor
C:GA
Mutationsrobhgie
N:
HCSelection: u' ∈ U' s.t.

ρ(ℳ(u′), φ) is small
20

M. Waga (NII)Robustness-Guided Equivalence Test
[Contribution]

Gen. population U

U := U'~∀u ∈ U . ℳ(u) = ℳ(u) ?
YesGen. next population U'

Selection: u' ∈ U' s.t.

ρ(ℳ(u′), φ) is small
20

No

Return u&revossor
C:GA
Mutationsrobhgie
N:HCOnly ℳ
Continuous
M. Waga (NII)Why ρ(ℳ(u′), φ) as Fitness?
Assumption: ℳ /⊧ φi.e. ∃u.ρ(ℳ(u), φ) ≤ 0Robustness~x ρ(ℳ(u′), φ) + ρ(ℳ(u′), φ)~

Fact: ℳ ⊧ φ i.e.

x+~∀u . ρ(ℳ(u), φ) ≥ 0x+x

by model checking

x++x

Heuristic: Find u' s.t.
~ℳ(u′) ≠ ℳ(u′) inρ(ℳ(u′), φ) is small

0x++x+
Input u'~21

M. Waga (NII)Why ρ(ℳ(u′), φ) as Fitness?
Assumption: ℳ /⊧ φi.e. ∃u.ρ(ℳ(u), φ) ≤ 0Robustness~x ρ(ℳ(u′), φ) + ρ(ℳ(u′), φ)~

Fact: ℳ ⊧ φ i.e.

x+~∀u . ρ(ℳ(u), φ) ≥ 0x+xby model checkingx

Heuristic: Find u' s.t.
~ℳ(u′) ≠ ℳ(u′) inρ(ℳ(u′), φ) is small

0x++x++x+
Input u'~ℳ and ℳ deviate
21

M. Waga (NII)How About Direct Comparison?
•Direct comparison is also available e.g. [Abbas+,MEMOCODE’14]•Potential Issue: more local maxima

Cont. vs Cont.
OutputCont. vs Disc.
Output

ℳ′(u)

ℳ′(u)

ℳ(u)

ℳ(u)

Input

Input
22

M. Waga (NII)Outline•

Introduction•

Preliminary: Black-box checking••Main Contribution:
Robustness-guided equivalence test••

Automata learning, model checking, & equiv. test

idea: Optimization + robustness

Experiments
23

M. Waga (NII)Research Questions

RQ1: Does RobBBC falsify as many spec. as baseline?
RQ2: Which BBC is the best: Random, GA, and HC?
RQ3: Scalable wrt # of spec?

24

M. Waga (NII)Experiment Setting: Algorithms•

Robustness-guided BBC with•

Genetic Algorithm (RobBBC(GA))•Hill Climbing (RobBBC(HC))

Ours

•

BBC (equivalence test by random search)•

Breach: one of the SoTA falsification tools•

Pure random search•Baselineshow the diﬃculty of the specifications
25M. Waga (NII)Experiment Setting: Benchmark
Model: Automatic Transmission [Hoxha+,ARCH’14-15]
Spec: Set of STL formulas'1'2'3'4'5'6'7•

Similar specifications with diﬀerent thresholds•Motivation: hard to decide the threshold

STL template⇤(v < p)⇤(g = 3 ) v > p)⌃[p1 ,p2 ] (v < p3 _ v > p4 )⇤[0,26] (v < p1 ) _ ⇤[28,28] (v > p2 )⇤(! < p1 _ X (! > p2 ))⇤(v < p1 ) ⇤[0,p2 ] (v < p3 ))⇤(((g 6= p1 ) ^ X (g = p1 )) ) ⇤[0,p2 ] (g = p1 ))parameter valuations
p 2 {100, 102.5, 105, 107.5, 110, 112.5, 115, 117.5, 120}p 2 {20, 22.5, 25, 27.5, 30}(p1 , p2 ) 2 {(5, 20), (5, 25), (15, 30), (10, 30)}, (p3 , p4 ) 2 {(50, 60), (53, 57)}
p1 2 {90, 100, 110}, p2 2 {55, 65, 75}
p1 2 {4000, 4700}, p2 2 {600, 1000, 1500}
p1 2 {30, 40, 50}, p2 2 {6, 8, 10}, p3 2 {60, 70, 80, 90}
p1 2 {1, 2, 3, 4}, p2 2 {1, 2, 3}

26size9589636
12M. Waga (NII)

# of Falsified Properties# of Properties
RobBBC(HC)RobBBC(HC)

Random BBC

RobBBC(GA)RobBBC(GA)

BreachPure Random

10.75
0.5
0.25
0φ1φ2φ3φ4φ5φ6•

RobBBC(HC) and Breach: Often fails•Random BBC: sometimes fails•

RobBBC(GA): the largest for all specifications

27φ7M. Waga (NII)

# of Falsified Properties# of Properties
RobBBC(HC)RobBBC(HC)

Random BBC

RobBBC(GA)RobBBC(GA)

BreachPure Random

10.75
0.5
0.25
0φ1φ2φ3φ4φ5φ6•

RobBBC(HC) and Breach: Often fails•

Random BBC: sometimes fails•

RobBBC(GA): the largest for all specifications

RQ1: Yes, RobBBC canfalsify as many as Breach
27φ7

M. Waga (NII)

# of Falsified Properties# of Properties
RobBBC(HC)RobBBC(HC)

Random BBC

RobBBC(GA)RobBBC(GA)

BreachPure Random

10.75
0.50.25
0φ1φ2φ3φ4φ5φ6•

RobBBC(HC) and Breach: Often fails•Random BBC: sometimes fails•RobBBC(GA): the largest for all specifications

RQ1: Yes, RobBBC canfalsify as many as Breach
27φ7

RQ2: GA falsified more thanRandom and HC…
M. Waga (NII)

Time to Falsify by the Fastest Method
Time to Falsify
Random BBC

RobBBC(HC)RobBBC(HC)RobBBC(GA)RobBBC(GA)

Breach

10.75
0.5
0.25
0φ1

•φ2φ3φ4φ5φ6φ7

RobBBC(GA) tends not be the fastest when others
are available → not the best for easy spec.

28

M. Waga (NII)

Time to Falsify by the Fastest Method
Time to Falsify
Random BBC

RobBBC(HC)RobBBC(HC)RobBBC(GA)RobBBC(GA)

Breach10.75
0.50.250φ1•

φ2φ3φ4φ5φ6φ7

RobBBC(GA) tends not be the fastest when others
are available → not the best for easy spec.
RQ2: GA falsified more than Random HC
For easy spec. Random BBC can be an option
28M. Waga (NII)Scalability wrt # of Spec. in φ6
Execution time [sec.]

Random BBC
RandomBBCRobBBC(HC)RobBBC(HC)RobBBC(GA)RobBBC(GA)
BreachBreach2500
20001500≈ linear≈ constant

1000
500
005101520253035# of the falsified properties

RQ3: BBC is more scalable than Breach
wrt # of Spec.
29

M. Waga (NII)Conclusion•

Introduced robustness-guided BBC••

Equivalence test using robustness

Experimental evaluation•

It outperforms Breach30

M. Waga (NII)Conclusion•

Introduced robustness-guided BBC••

Equivalence test using robustness

Experimental evaluation•It outperforms Breach
But this is the beginning of the story…
30

M. Waga (NII)~Direct Reuse of ℳ Does Not Work

Cyber-Physical Systems with Robustness-Guided Black-Box Checking

HSCC ’20, April 22–24, 2020, Sydney, NS

sult of falsi�cation only using the extracted Mealy machine. The second column shows thModelchecking
generates
nterexamples found by model checking of the Mealy machines M̃ extracted during the BBC.
false countercon�rmed
examplesows the number of the actual counterexamples
through a simulation of the CPS
and the �fth columns show the average and the standard deviation of the robustness, respe
STL formula⇤( < 90)⇤[0,26] ( < 90) _ ⇤[28,28] ( > 40)⇤[0,26] ( < 90) _ ⇤[28,28] ( > 50)⇤[0,26] ( < 90) _ ⇤[28,28] ( > 60)
R�����HC

GA# ofB�����

# of6 |= M̃
10410106 |= M
5000

Average of J K
1.10
4.19
3.80
3.24

std. dev. of J K
1.94
0.00
0.60
0.76

Table 4: Average of the number of the states
But robustness
is lowtracted Mealy
machineR�����
1
2
3
4
5

31

6,tiny6,small

181.90612.60154.201372.70948.60
26.60
45.30

HCGA

270.90441.50661.60610.00200.20198.301194.70 1353.30
1442.14888.6035.20
M.32.10
Waga (NII)
40.60
39.50

Future Work•How to (re-)use the generated Mealy machine?

•Black-box checking for multiple systems••

Adaptive model checking?

Try more benchmarks to figure out further issues

32

M. Waga (NII)

Appendix
33

M. Waga (NII)Experiment Setting (Detail)•Executed each same experiment setting 10 times••

We used the average

Amazon EC2 c4.large (2 vCPUs and 3.75 GiB RAM)

34

M. Waga (NII)