和賀 正樹, Étienne André & 蓮尾一郎, NII / 総研大
動機• シミュレーションやプロトタイプ実装から• どこが危険か (例: 10s–14sが危険だった)• CPSではモデル検査は困難

膨大なログが得られる• ログから何らかの性質を探したい• どういう時間制約で危険か• black-box component• 環境など未知の情報• 代わりにシステムのログから異常を検知したりフィードバックする必要がある

o(例: 遅いと困るが、具体的な期限は不明)• 例: 怪しい挙動• どういうデータで危険か• 人力で探すのは大変(例: 弱い加減速は強い加減速より頻繁にある)パラメタ付き時間制約への拡張

時間パターンマッチング
MONAA: https://github.com/MasWag/monaa

データ付きイベントへの拡張

パラメタ付き時間パターンマッチング

記号的モニタリング

ParamMONAA: https://github.com/MasWag/monaa/tree/PTPM

例1: 高頻度な加減速の検出

SyMon: https://github.com/MasWag/symon

例: 高頻度な加減速の検出• 入力1 (仕様): p秒間に3回以上の強さ[a,b]の加減速は異常

例1: 高頻度な加減速の検出↑数値データのパラメタ!!
20秒が適切か?• 入力1 (仕様): p秒間に3回以上の加減速は異常 どれくらいの加減速か?

• 入力1 (仕様): 20秒以内に3回以上の加減速は異常↑ 時間制約!!

• 入力2 (ログ):• 入力2 (ログ):↑ パラメタ付き時間制約!!

Accel

BrakeAccel

01

815

Brake Accel

20

Brake Accel

232730BrakeAccel

3440

例えば14.5秒から34.4秒で異常!!

t• 入力2 (ログ):Accel

BrakeAccel

01815• 出力: {(t,t′) | 8 ≦ t < 15, 34 < t′ ≦ 40}
無限個あるので制約式で出力

Brake Accel20

Brake Accel

2327

BrakeAccel

34

40

30

tAccel(30)Brake(25)

Accel
(10)

01

815

• 時間オートマトン (TA)40

• 0.7秒から28秒でp=26で異常!!

• 14.5秒から34.4秒でp=19、a=1、b=10で異常!!

t⋮

• 出力:

⋮

{(t, t′, p,a,b) | 0 ≦ t < 1, 27 < t′ ≦ 30, p = 26, a ≦ 4, b ≧ 30}∪ {(t, t′, p,a,b) | 0 ≦ t < 1, 34 < t′ ≦ 40, p = 33, a ≦ 1, b ≧ 30}∪ {(t, t′, p,a,b) | 8 ≦ t < 15, 34 < t′ ≦ 40, p = 19, a ≦ 1, b ≧ 10}
区間 + パラメタの値の制約式で出力$

例2: 値と周期の関係の同定

例2: 未知の周期の同定
実行時間• 入力1 (仕様):

Table 1. Execution time (sec.)
MONAA(TRE)
7.03
7.55
8.05
8.54
9.16
9.53
10.05
10.53
11.05

withdraw(n, a), vp = nc tp1 < 100"v1 := v1 + a"c = tp2(仕様):
withdraw(n, a) c = tp
v2 := v2 + a •c 入力1
tp 2 (50, 100)

MONAA
(TA)
0.80
1.27
1.73
2.21
2.69
3.14
3.60
4.06
4.56

libmonaa(TA ishard coded)

Montre(online)

0.20
0.31
0.42
0.53
0.64
0.75
0.85
0.971.07

0.13
37.45
75.93
115.88153.71
189.55216.92260.77289.631

既存研究$, t < 10A
AS /x := 0

Montre(offline)
0.03
1.56
3.13
4.69
6.21
7.75
9.33
10.88
12.39

127,552
16,312
10,8087,464
45,700255,750
16,312
10,752
7,308
65,764
383,168
16,344
10,692
7,308
87,928508,756
16,468
10,8407,288
99,540
時間パターンマッチング
632,484
16,28010,9007,452
109,076
758,500
16,34010,768
7,292
147,048• (Theory Paper) Masaki Waga, Ichiro Hasuo, and Kohei Suenaga Efficient
894,692
16,46810,696
7,440
153,992
Online Timed Pattern Matching by Automata-Based Skipping Proc.
1,011,426
16,312
10,808
7,288
166,660
FORMATS
2017, LNCS
10419, p.
224-243.

参考文献

Table
2 MasakishowsWaga,
that Ichiro
the memoryof MONAA
is inde• (ToolPaper)
Hasuo, andusage
Kohei Suenaga
MONAA:
ATool for Timed
Matching
Automata-BasedAccelerationProc.
pendentof thePatternlengthof thewith
timed
word, whilethat of Montre
MT-CPS 2018, p. 14-15.
offline depends.

パラメタ付き時間パターンマッチング

References• Étienne André, Ichiro Hasuo, and Masaki Waga Offline timed pattern[1] R. Aluranduncertainty
D.L. Dill. Proc.
A theoryof timed
Theor. Comput.
matching
underICECCS
2018,automata.
IEEE.

Sci., 126(2):183–235, 1994.

[2] E. Asarin,P. Caspi
andAndréO. Maler.
regularexpressions.
J. ACM,• Masaki
Waga andÉtienne
OnlineTimed
Parametric
Timed
Pattern Matchingwith 49(2):172–206,
Automata-Based2002.
Skipping To appear in Proc. NFM 2019.
[3] R.S. Boyer and J.S. Moore. A fast string searching algorithm. Com記号的モニタリング
mun. ACM, 20(10):762–772, 1977.
• MasakiWaga, Étienne
André, andIchiro
Hasuo
Symbolic
Monitoring[4] F. Franek,C.G. Jennings
andW.F.
Smyth.
A simplefast against
hybridSpecifications Parametric in Time and Data To appear in Proc. CAV 2019.

pattern-matching algorithm. J. Discrete Algorithms, 5(4):682–695,
2007.

0startVS, x < p2 , t < 10/x := 0, y := 0

VS /x := 0, y := 0l03

v1 := 0, v2 := 0$, t < 10AS,x < p1 , t < 10/x := 0AS, x < p1 , t < 10/x := 00AV12v1 > v2

l1

withdraw(n, a), vp 6= nc tp1 < 100, v2 := v2 + al2withdraw(a)a  vpl0withdraw(a)a > vptp1  c  tp2
c := 0間隔[tp1,tp2] で vp以上引き出されている

VFig. 3: PTDAs
in Dominant (left) and Periodic (right)• 入力2 (ログ):429x < 5.3
timed pattern matchingVS,p2 , p3 < yEncoding< p4 , t < 10/x :=parametric0, y := 0• 入力2 (ログ):The symbolic monitoring problem is a generalization of the parametric timed
間隔: 短間隔:problem
長431
pattern matchingof [4]. Recall that parametric timed pattern matching432
aims at synthesizing
timing parameter valuations and start and end times in theAS VS AS VS AS VS
ASVSAS…433 log for which a log segment satisfies or violates a specification. In our approach,
7 parameters時刻434
by adding a clock measuring
absolute time, and two timing
encoding
tCopy
8.5
9.0
0.1 0.3 0.7 0.8
1.4 1.6
10.5
435
respectively the start and end date of the segment, one6 can easily infer the log
出力:436
segments for which the property is •satisfied.
100
tp15tp2• 出力:437Consider the Dominant PTDA (left of Fig. 3).
Itisinspiredbya
mon80 4438 v(pitoringof v(pwithdrawals
from bank accounts of various users [15]. This PTDA{(t,t′,v) | t ∈ [0,0.1), t′ ∈ (1.4, 1.6],1) > 0.6,2) > 0.2, …}
60
439
monitors situations when a user withdraws more than3 half of the total with∪ … ∪ {(t,t′,v) | t ∈ [1.6, 8.5), t′ ∈ (10.5,∞),v(p1) >within
1.5,v(pa2) time> 0.5}window of (50, 100). The actions40 2 are ⌃ = {withdraw}
440
drawals441
and Dom(withdraw) = {n, a}, where n has a string
and a has an inte20 value
1442
ger value. The string n represents a user name and the integer a represents the0 0443
amount of the withdrawal by the user n. Observe thatneverreset,
01000
2000
4000 30 50000clock
5 c is1015 3000
20 2535 40
 (vp)444
and therefore measures absolute time. The automaton can non-deterministically
Numberof events [⇥1, 000]
445
remain in l0 , or start to measure a log by taking the "-transition to l1 checking
Fig. 4:
Execution
446
c = tp1 , and therefore “remembering” the start time using timing
parameter
tp1 . time (left) and mem
447
Then, whenever a user vp has withdrawn more than half of the accumulated
448
withdrawals (data guard 2v1 > v2 ) in a (50, 100) time
160window (timed guard
No Skip Param. Skip. Non-Pram.
参考: MONAA
Dominant
449
c tpSkip
totheaccepting
loca1 2 (50, 100)), the automaton takes a "-transition
140
Periodic
1,467
0.032
0.040.05 checking< c0.01
450tion,= tp2 , and therefore remembering the120
end time using timing
2,837
0.07
0.071
0.0805451
parameter tp2<. 0.01
100
4,595
0.113
0.112
0.121
0.01
80
5,839 0.1425
0.1405
0.151
0.01
7,301
0.182
0.17550.19050.01
60
452
6 Experiments
8,995
0.222
0.2125
0.225
0.01
40
10,3150.26
0.24150.26150.010520
11,831 0.295
0.271
0.0125453 0.2935
We implemented
our symbolic monitoring algorithm in a 0tool SyMon in C++,
13,183 0.3205
0.29550.32050.02 for data is the strings and the integers.
454
where the domain
2 We
4 use
6 8PPL10 [8]
12 14 16 18 20
14,657 0.361
0.33150.35350.02representation of the valuations. We note that we employ an455
for the symbolic
Number of events [⇥1, 000]456
optimization to merge adjacent polyhedra in the configurations if possible. WeFig. 5: Execution time (left) and memory usag
430

実行時間 (ログ長 vs. 秒)

Memory Usage [KB]

A

Memory Usage [KB]

B

引き出し額

A

Execution time [sec.]

BA

306
127,552
255,750
383,168
508,756
632,484
758,500
894,692
1,011,426

34

B, c < 20

Ac := 0Length oftimed word30

区間 + パラメタの値の制約式で出力

例:
start

27Accel(15)• 0.7秒から28秒でp=26、a=4、b=30で異常!!

{(t, t′, p) | 0 ≦ t < 1, 27 < t′ ≦ 30, p = 26}∪ {(t, t′, p) | 0 ≦ t < 1, 34 < t′ ≦ 40, p = 33}∪ {(t, t′, p) | 8 ≦ t < 15, 34 < t′ ≦ 40, p = 19}

例: (ABAB(AB)+)%(0,20)$

23

Brake(4)

例えば

• 出力:

• 時間正規表現 (TRE)20

Brake Accel(4)
(1)

例えば

• 14.5秒から34.4秒でp=19で異常!!

仕様記述言語

Brake Accel(5)(6)

Execution time [sec.]esutna).

• 単に安全/危険のみではなくより多くの情報を探せた• システムの正しさを保証したいaa. • 高速
約50倍
約3倍
Table 2. Memory usage (kbytes)a • オンライン (動作中のシステムに適用可能)
libmonaa
Length ofMONAA
MONAAMontre(TAisetimed word(TRE)(TA)(offline)
hard coded)
nt
306
16,46810,8087,308
27,456surad

貢献• 開発プロセスでもモニタリングは重要

tp1  tp2 ( )rg
et,odses

時間パターンマッチングによるCPSのモニタリング

実行時間