-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathREADME.html
454 lines (446 loc) · 17.4 KB
/
README.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml" lang="" xml:lang="">
<head>
<meta charset="utf-8" />
<meta name="generator" content="pandoc" />
<meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes" />
<title>README</title>
<style>
html {
line-height: 1.5;
font-family: Georgia, serif;
font-size: 20px;
color: #1a1a1a;
background-color: #fdfdfd;
}
body {
margin: 0 auto;
max-width: 36em;
padding-left: 50px;
padding-right: 50px;
padding-top: 50px;
padding-bottom: 50px;
hyphens: auto;
overflow-wrap: break-word;
text-rendering: optimizeLegibility;
font-kerning: normal;
}
@media (max-width: 600px) {
body {
font-size: 0.9em;
padding: 1em;
}
h1 {
font-size: 1.8em;
}
}
@media print {
body {
background-color: transparent;
color: black;
font-size: 12pt;
}
p, h2, h3 {
orphans: 3;
widows: 3;
}
h2, h3, h4 {
page-break-after: avoid;
}
}
p {
margin: 1em 0;
}
a {
color: #1a1a1a;
}
a:visited {
color: #1a1a1a;
}
img {
max-width: 100%;
}
h1, h2, h3, h4, h5, h6 {
margin-top: 1.4em;
}
h5, h6 {
font-size: 1em;
font-style: italic;
}
h6 {
font-weight: normal;
}
ol, ul {
padding-left: 1.7em;
margin-top: 1em;
}
li > ol, li > ul {
margin-top: 0;
}
blockquote {
margin: 1em 0 1em 1.7em;
padding-left: 1em;
border-left: 2px solid #e6e6e6;
color: #606060;
}
code {
font-family: Menlo, Monaco, 'Lucida Console', Consolas, monospace;
font-size: 85%;
margin: 0;
}
pre {
margin: 1em 0;
overflow: auto;
}
pre code {
padding: 0;
overflow: visible;
overflow-wrap: normal;
}
.sourceCode {
background-color: transparent;
overflow: visible;
}
hr {
background-color: #1a1a1a;
border: none;
height: 1px;
margin: 1em 0;
}
table {
margin: 1em 0;
border-collapse: collapse;
width: 100%;
overflow-x: auto;
display: block;
font-variant-numeric: lining-nums tabular-nums;
}
table caption {
margin-bottom: 0.75em;
}
tbody {
margin-top: 0.5em;
border-top: 1px solid #1a1a1a;
border-bottom: 1px solid #1a1a1a;
}
th {
border-top: 1px solid #1a1a1a;
padding: 0.25em 0.5em 0.25em 0.5em;
}
td {
padding: 0.125em 0.5em 0.25em 0.5em;
}
header {
margin-bottom: 4em;
text-align: center;
}
#TOC li {
list-style: none;
}
#TOC ul {
padding-left: 1.3em;
}
#TOC > ul {
padding-left: 0;
}
#TOC a:not(:hover) {
text-decoration: none;
}
code{white-space: pre-wrap;}
span.smallcaps{font-variant: small-caps;}
span.underline{text-decoration: underline;}
div.column{display: inline-block; vertical-align: top; width: 50%;}
div.hanging-indent{margin-left: 1.5em; text-indent: -1.5em;}
ul.task-list{list-style: none;}
.display.math{display: block; text-align: center; margin: 0.5rem auto;}
</style>
<!--[if lt IE 9]>
<script src="//cdnjs.cloudflare.com/ajax/libs/html5shiv/3.7.3/html5shiv-printshiv.min.js"></script>
<![endif]-->
</head>
<body>
<h1 id="fast-falsification-with-adaptive-inputs">Fast Falsification with
Adaptive Inputs</h1>
<p>FalStar is a tool for the falsification of hybrid systems. It takes
as an input a model (currently: Simulink) and a configuration file and
tries to come up with an input signal such that the output signal
produced by the model falsifies given requirements.</p>
<p>Requirements</p>
<ul>
<li>Java 1.8, Scala 2.12 (compile time only)</li>
<li>Matlab (tested different versions after R2017)</li>
</ul>
<p>Contact: gidonernst (*) gmail.com</p>
<ul>
<li><p>Gidon Ernst, Sean Sedwards, Zhenya Zhang, Ichiro Hasuo: <em>Fast
Falsification of Hybrid Systems using Probabilistically Adaptive
Input</em>, QEST 2019, Preprint: <a
href="https://arxiv.org/abs/1812.04159"
class="uri">https://arxiv.org/abs/1812.04159</a></p></li>
<li><p>Gidon Ernst, Sean Sedwards, Zhenya Zhang, and Ichiro Hasuo:
<em>Falsification of hybrid systems using adaptive probabilistic
search</em>, Transactions on Modeling and Computer Simulations,
2021</p></li>
</ul>
<h2 id="quickstart">Quickstart</h2>
<p>Determine MATLAB path</p>
<pre><code>./falstar-config.sh</code></pre>
<p>Compile <code>falstar.jar</code></p>
<pre><code>make compile</code></pre>
<p>Test whether everything worked</p>
<pre><code>./falstar.sh # prints usage instructions
make test # run a simple test case</code></pre>
<p>This falsifies a Simulink model of an automatic transmission against
specification <code>always_[0,30] speed < 120</code> and displays
various input and output signals. Here’s the output:</p>
<pre><code>trial 1/1
property always_[0.0, 30.0] speed < 120.0
algorithm adaptive
control points: 2 2 3 3 3 4
exploration ratio: 0.25
budget: 100
starting matlab ... connected (4s)
initializing 'automatic_transmission' ... done (17s)
......
inputs
t__ = [0.0; 10.0; 25.0; 30.0]
u__ = [75.0 0.0; 100.0 0.0; 37.5 243.75; 37.5 243.75]
falsified with robustness -6.849703872580591
statistics
simulations 6
total time 29s
peak memory 37111 kb
bye</code></pre>
<p>If you’re tired of waiting for Matlab to initialize on every trial,
you can keep an active instance running. Be aware that this caches
initialized models as well, so if you change those, you need to restart
the session. It’s a simple command line interface to Matlab (currently
without error handling, and it will terminate if you type in an invalid
command).</p>
<pre><code>./falstar-session.sh</code></pre>
<h2 id="simulink-model-set-up">Simulink model set up</h2>
<p>Simulink models are accessed through their input and output ports and
through the Matlab function <code>sim</code>. The model must currently
be prepared for use as follows</p>
<ul>
<li>In the model configuration parameter setup, set the input to
<code>[t__, u__]</code>. This will cause the simulation to read these
two variables off the workspace and interpret them as the simulation
input. <code>t__</code> is a column matrix of time points and
<code>u__</code> provides the corresponding input vectors in each row
for the respective time points (see an example above). The falsification
tool provides these variables to the Matlab simulation engine in this
form.</li>
<li>The output signal should be recorded to <code>tout</code> and
<code>yout</code> (which are the default settings).</li>
<li>Make sure the output signal is not truncated</li>
<li>Make sure that the <em>interpolation settings</em> on the input
ports are as desired, for piecewise constant inputs disable
interpolation.</li>
</ul>
<h2 id="command-line-options">Command line options</h2>
<pre><code>usage: falstar [-dv] file_1 ... file_n
-d dummy run, parse and validate configuration only
-v be more verbose</code></pre>
<p>In particular, the <code>-v</code> flag shows all interaction with
the Matlab engine.</p>
<h2 id="configuration-file-syntax">Configuration file syntax</h2>
<p>The syntax is S-expression based. Line comments are introduced with
<code>;</code>.</p>
<p>FalStar maintains a context, consisting of</p>
<ul>
<li>a currently selected system on which it operates</li>
<li>a currently selected falsification method</li>
</ul>
<p>relative to which formulas are interpreted (e.g., parameter and
input/output signal names). Similar to SMT-LIB, contexts can be saved
and restored with</p>
<pre><code>(push)
...
(pop)</code></pre>
<p>The configuration file can be composed of multiple parts, where
<code><path></code> is a doubly-quoted path that is interpreted
relative to the working directory of FalStar:</p>
<pre><code>(include <path>)</code></pre>
<p>The path is relatve to the <em>inluding</em> file, except when it
starts with ‘.’ or with ‘/’ then it is used as given.</p>
<p>System declarations (see below) and requirements for some models are
in the <code>models</code> subfolder, ready to be used.</p>
<h3 id="selecting-a-system-model">Selecting a system model</h3>
<p>See <code>src/resource/configuration/test.cfg</code> for an example.
Currently supported system types: <code>simulink</code> and
<code>matlab</code>.</p>
<pre><code>(define-system <identifier>
; two alternative ways to set up systems
(simulink <path> [<load>])
(matlab <name> <path> <init> <run>)
; common configuration options
(parameters p1 ... pk)
(inputs i1 ... in)
(outputs o1 ... om)
; valid input ranges
(constant pi <num>)
(constant pi <num> <num>)
(constant ij <num>)
(constant ij <num> <num>)
(piecewise-constant ij <num> <num>)
)</code></pre>
<p>A system definition comprises of a declaration of how the simulation
is executed, by a <code>simulink</code> or <code>matlab</code> clause,
followed by a declaration of the system’s interface in terms of
parameters, input, and output ports; and a declaration of valid ranges
reps. values for these which can later be overriden if desired</p>
<h4 id="system-type-simulink">System Type: <code>simulink</code></h4>
<p>A simulink system is declared by</p>
<pre><code>(simulink <path> [<load>])</code></pre>
<p>where <code><path></code> must point to a <code>.mdl</code> or
<code>.slx</code> file. An optional list <code><load></code> of
<code>.m</code> files or <code>.mdl</code> files can be specified. The
initialization sequence runs</p>
<pre><code>addpath(<dir>) % where <dir> is the directory containing <path>
load_system(<name>) % where <name> is the file name stem (without suffix)
<load> % execute .m files without suffix
load(<load>) % load .mat files</code></pre>
<p>and each simulation is executed with the <code>sim</code> function,
where the stopping time and the external inputs are explicitly given by
Falstar (i.e., those defined in the model are overriden).</p>
<h4 id="system-type-matlab">System Type: Matlab</h4>
<p>A system scripted in Matlab is declared by</p>
<pre><code>(matlab <name> <path> <init> <run>)</code></pre>
<p>where <code><name></code> is an arbitrary identifier (implicit
for Simulink systems from the file name), <code><path></code> is
the base path where scripts are located, and <code><init></code>
and <code><run></code> are two Matlab functions used to initialize
the system and run simulations respectively.</p>
<p>Falstar executes initially</p>
<pre><code>addpath(<path>)
<init></code></pre>
<p>and for each simulation</p>
<pre><code><run>(p, u, T)</code></pre>
<p>where <code>p</code> is an array of values for the parameters,
<code>u</code> is a time-varying input signal, and <code>T</code> is the
stopping time. The expected result is a pair <code>[tout, yout]</code>
describing the output trace, in the same format as <code>.tout</code>
and <code>.yout</code> from the <code>Array</code> format specified for
Simulink systems.</p>
<h4 id="interface-description">Interface Description</h4>
<p>The interface description consists of</p>
<ul>
<li>Parameters <code>p1</code>, …, <code>pk</code>, which are names of
MATLAB variables that will be initialized by FalStar</li>
<li>Inputs <code>i1</code>, …, <code>in</code>, which give names to
top-level input ports of the Simulink system (<code>In</code> blocks),
in order of their numbers in Simulink (the names attached to the ports
in the model are ignored)</li>
<li>Outputs <code>o1</code>, …, <code>om</code>, analogously for the
output ports (<code>Out</code> blocks)</li>
</ul>
<h4 id="definining-input-ranges">Definining Input Ranges</h4>
<p>The following lines declare the ranges of parameters and inputs, one
statement for each.</p>
<ul>
<li>Patamerets <code>pi</code> can be either a fixed constant value or a
range, from which the value is chosen during falsification.</li>
<li>Inputs <code>ii</code> can be either a fixed value, a constant input
signal, or a piecewise constant input signal, again with a range of
values in the latter two cases. Note that the time intervals for which
these are held constant depends on the configuration of the
falsification solver.</li>
</ul>
<h4 id="selecting-a-system">Selecting a System</h4>
<p>More than one system can be defined within a Falstar script. You can
pick the system that is going to be used for the subsequent
falsification attempts or for validation:</p>
<pre><code>(select-system <identifier>
<overrides>)</code></pre>
<p>where <code><identifier></code> refers to a previously declared
system, and <code><overrides></code> are
<code>(constant ...)</code> or <code>(piecewise-constant ...)</code>
definitions that can be used to override some of the settings from the
system declaration. This comes in handy if a system has several modes of
operation (like the Powertrain model).</p>
<h3 id="terms-and-formulas">Terms and Formulas</h3>
<p>May refer to signal names (defined by the current model)</p>
<p>Arithmetic operators:
<code>< > <= >= == != + - * / abs in</code><br />
Logical connectives:
<code>! => || && true false not implies and or always eventually</code><br />
For example</p>
<ul>
<li><code>(abs (* 1.5 x))</code> denotes the absolute value of
<code>1.5 x</code> where <code>x</code> is a signal name</li>
<li><code>(in x a b)</code> = <code>(and (<= a x) (<= x b))</code>
asserts that <code>x</code> lies in the range <code>[a,b]</code></li>
<li><code>(always (10 30) phi)</code> asserts that subformula
<code>phi</code> holds over time interval <code>[10,30]</code></li>
</ul>
<h3 id="definitions">Definitions</h3>
<p>Abbreviations, which are really just macros, can be defined as</p>
<pre><code>(define <id> <S-Expr>)</code></pre>
<p>These are expanded immediately when encountered in certain places,
but interpreted only alongside the surrounding context. Definitions are
expanded in formulas and almost in all places where numbers are
expected.</p>
<h3 id="falsification">Falsification</h3>
<p>First, a falsification method has to be selected. Currently the
following are supported</p>
<ul>
<li><p>Random sampling
<code>(set-solver random <cp> <max-iter>)</code>, where
<code><cp></code> denotes the number of control points/segments of
piecewise constant input signals and and <code><max-iter></code>
is the upper bound of iterations/simulations to run</p></li>
<li><p>Adaptive probabilistic search
<code>(set-solver adaptive (<cp1> <cp2> ...) <exploration> <max-iter>)</code>,
where <code><cp1></code>, <code><cp2></code>, … declares an
(increasing) sequence of <em>granularity levels</em> with the
corresponding number of control points, <code><exploration></code>
is the exploration ratio (a good value is <code>0.25</code>) and
<code><max-iter></code> is the maximum number of
iterations</p></li>
</ul>
<p>Moreover, the following bridge might still work (untested):</p>
<ul>
<li>Breach
<code>(<set-solver breach <cp> <opt> <max-iter>)</code>
selects falsification by Breach with <code><cp></code> control
points, optimization method <code><opt></code> (from
<code>cmaes</code>, <code>global_nelder_mead</code>, …)</li>
</ul>
<p>Requirements can be falsified by</p>
<pre><code>(falsify <formula1> <formula2> ...)</code></pre>
<p>Results are logged to in <code>.csv</code> format if specified (in
double quotes, relative to the current file FalStar). The log file
collects entries for each individual falsification trial, whereas the
report groups them together (cf. <code>(set-repeat _)</code> below) with
aggregated information on number of simulations, running time, and
success rate.</p>
<pre><code>(set-log <path>)
(set-report <path>)</code></pre>
<p>Usually, log and report are written only at the end, but they can be
flushed eagerly with <code>(flush-log)</code>, which reads in any
previous values stored in that file and integrates the new results. It
is important to note that different solvers produce different columns in
the table, such that this merging is necessary.</p>
<p>The initial random seed can be specified by</p>
<pre><code>(set-seed <number>)</code></pre>
<p>To request each falsification trial <code>(falsify ... )</code> to be
repeated multiple times (with different seeds)</p>
<pre><code>(set-repeat <num>)</code></pre>
<h3 id="validation-scripts">Validation Scripts</h3>
<p>The general procedure for validation is described separately in file
<code>Validation.md</code>. In order to make use of this feature, one
has to provide particular scripts as follows. First, set up where the
results should be stored, in a similar format to falsification runs.
Both files will be in <code>.csv</code> format, existing files with
results are extended.</p>
<pre><code>(set-log <path>)
(set-report <path>)</code></pre>
<p>In order to validate, one can give the path to a <code>.csv</code>
file simply by</p>
<pre><code>(validate <path>)</code></pre>
<p>This assumes that all models referred to by this
<code><path></code> in terms of their mnenonic codes have been set
up properly in the script before this line.</p>
</body>
</html>