Trace-Checking Signal-based Temporal Properties: A Model-Driven Approach

Talk at ASE 2020

1. .lu
software verification & validation
VVS
Trace-Checking
Signal-based Temporal Properties:
A Model-Driven Approach
Chaima BOUFAIED, Claudio MENGHI, Domenico BIANCULLI, Lionel BRIAND, Yago ISASI PARACHE

2. Trace Checking (1)
•Run-time verification technique
•Traces represent system executions
•Properties are based on the system’s requirements
•Uses an automated decision procedure to check properties on
traces
!2

3. Trace Checking (2)
•In this work, we consider tools that:
•support declarative specification formalisms for expressing
requirements
•are deployed at offline stage
•yield a Boolean verdict using qualitative semantics
!3

4. Context
!4
Industrial case study in the
aerospace domain

5. Signal-based Temporal Properties
(SBTPs)
•SBTPs characterize the
behavior of the system when its
inputs and outputs are signals
over time
• “The velocity of the satellite
along the X-axis-Vel may
oscillate with a maximum
amplitude of 8000 km/h and a
maximum period of 180 min”
!5
t3t5
vl
vu
p1
p2
p3p5
p4
p2pAmp
period
time
signal value

6. Motivations
•SBTPs are common in many cyber-physical systems
•Several languages to express SBTPs (e.g., STL, STL*, SFO)
•either they are not expressive enough (e.g., STL)
•or they are not supported by efficient trace checking procedures (e.g., SFO)
•There is trade-off between languages expressiveness and trace checking
procedure efficiency
!6

7. Contributions
•SB-TemPsy: a Trace-Checking approach for SBTPs
•SBTemPsy-DSL: an expressive specification language for
SBTPs
•SBTemPsy-Check: an efficient trace-checking procedure
!7

8. SB-TemPsy-DSL:
Signal-Based Temporal Properties
made easy

9. Specification of
Temporal Properties
!9
Temporal
Logic
globally at most 2 P
before R at most 2 P
after Q at most 2 P
between Q and R at most 2 P
after Q until R at most 2 P
Domain-specific
Language (DSL)
•Syntax close to natural language
• Does not require a strong mathematical background
• Important for adoption among practitioners

10. SB-TemPsy-DSL
•Pattern-based specification language
•Supports the common types of SBTPs identified in a recent taxonomy
•Spikes, Oscillations
•Rise/Fall Time
•Overshoot/Undershoot
Chaima Boufaied, Maris Jukss, Domenico Bianculli, Lionel Claude Briand, and Yago Isasi Parache. 2019. Signal-Based
Properties: Taxonomy and Logic-based Characterization. CoRR abs/1910.08330 (2019), 1–39. arXiv:1910.08330 http: //
arxiv.org/abs/1910.08330
!10
*
*

11. SB-TemPsy-DSL
!11
exist oscillations in X-axis-Vel
with p2pAmp <= 8000
with period <= 180
•“The velocity of the satellite along the X-axis-Vel shall oscillate
with a maximum amplitude of 8000 km/h and a maximum period
of 180 min”

12. SB-TemPsy-DSL
!12
Propertyq::=q1andq2|q2orq1|notq|sc
Scope sc::=globallyp|beforetp|aftertp|attp|beforep1p
afterp1p|betweent1andt2p|betweenp1andp2p
Patternp::=assertc|sbecomes⇠v|ifp1then[withinùût]p2|
existsspikeins[with[width⇠v1][amplitude⇠v2]]|
existoscillationsins[with[p2pAmp⇠v1][period⇠v2]]|
srises[monotonically]reachingv|
sfalls[monotonically]reachingv|
sovershoots[monotonically]v1byv2|
sundershoots[monotonically]v1byv2
ùû::=exactly|at most|at least
Conditionc::=c1andc2|c1orc2|notc|s⇠v
t,t1,t22R;v,v1,v22R;⇠2{<,>,=,<,,$};
sis a signal in(or a mathematical expression over the signals in(
1
spike width amplitude

13. SB-TemPsy-DSL
!13
Propertyq::=q1andq2|q2orq1|notq|sc
Scope sc::=globallyp|beforetp|aftertp|attp|beforep1p
afterp1p|betweent1andt2p|betweenp1andp2p
Patternp::=assertc|sbecomes⇠v|ifp1then[withinùût]p2|
existsspikeins[with[width⇠v1][amplitude⇠v2]]|
existoscillationsins[with[p2pAmp⇠v1][period⇠v2]]|
srises[monotonically]reachingv|
sfalls[monotonically]reachingv|
sovershoots[monotonically]v1byv2|
sundershoots[monotonically]v1byv2
ùû::=exactly|at most|at least
Conditionc::=c1andc2|c1orc2|notc|s⇠v
t,t1,t22R;v,v1,v22R;⇠2{<,>,=,<,,$};
sis a signal in(or a mathematical expression over the signals in(
1
Oscillations p2pAmp period

14. SB-TemPsy-DSL
!14
Propertyq::=q1andq2|q2orq1|notq|sc
Scope sc::=globallyp|beforetp|aftertp|attp|beforep1p
afterp1p|betweent1andt2p|betweenp1andp2p
Patternp::=assertc|sbecomes⇠v|ifp1then[withinùût]p2|
existsspikeins[with[width⇠v1][amplitude⇠v2]]|
existoscillationsins[with[p2pAmp⇠v1][period⇠v2]]|
srises[monotonically]reachingv|
sfalls[monotonically]reachingv|
sovershoots[monotonically]v1byv2|
sundershoots[monotonically]v1byv2
ùû::=exactly|at most|at least
Conditionc::=c1andc2|c1orc2|notc|s⇠v
t,t1,t22R;v,v1,v22R;⇠2{<,>,=,<,,$};
sis a signal in(or a mathematical expression over the signals in(
1
rises

15. SB-TemPsy-DSL
!15
Propertyq::=q1andq2|q2orq1|notq|sc
Scope sc::=globallyp|beforetp|aftertp|attp|beforep1p
afterp1p|betweent1andt2p|betweenp1andp2p
Patternp::=assertc|sbecomes⇠v|ifp1then[withinùût]p2|
existsspikeins[with[width⇠v1][amplitude⇠v2]]|
existoscillationsins[with[p2pAmp⇠v1][period⇠v2]]|
srises[monotonically]reachingv|
sfalls[monotonically]reachingv|
sovershoots[monotonically]v1byv2|
sundershoots[monotonically]v1byv2
ùû::=exactly|at most|at least
Conditionc::=c1andc2|c1orc2|notc|s⇠v
t,t1,t22R;v,v1,v22R;⇠2{<,>,=,<,,$};
sis a signal in(or a mathematical expression over the signals in(
1
falls

16. SB-TemPsy-DSL
!16
Propertyq::=q1andq2|q2orq1|notq|sc
Scope sc::=globallyp|beforetp|aftertp|attp|beforep1p
afterp1p|betweent1andt2p|betweenp1andp2p
Patternp::=assertc|sbecomes⇠v|ifp1then[withinùût]p2|
existsspikeins[with[width⇠v1][amplitude⇠v2]]|
existoscillationsins[with[p2pAmp⇠v1][period⇠v2]]|
srises[monotonically]reachingv|
sfalls[monotonically]reachingv|
sovershoots[monotonically]v1byv2|
sundershoots[monotonically]v1byv2
ùû::=exactly|at most|at least
Conditionc::=c1andc2|c1orc2|notc|s⇠v
t,t1,t22R;v,v1,v22R;⇠2{<,>,=,<,,$};
sis a signal in(or a mathematical expression over the signals in(
1
overshoots

17. SB-TemPsy-DSL
!17
Propertyq::=q1andq2|q2orq1|notq|sc
Scope sc::=globallyp|beforetp|aftertp|attp|beforep1p
afterp1p|betweent1andt2p|betweenp1andp2p
Patternp::=assertc|sbecomes⇠v|ifp1then[withinùût]p2|
existsspikeins[with[width⇠v1][amplitude⇠v2]]|
existoscillationsins[with[p2pAmp⇠v1][period⇠v2]]|
srises[monotonically]reachingv|
sfalls[monotonically]reachingv|
sovershoots[monotonically]v1byv2|
sundershoots[monotonically]v1byv2
ùû::=exactly|at most|at least
Conditionc::=c1andc2|c1orc2|notc|s⇠v
t,t1,t22R;v,v1,v22R;⇠2{<,>,=,<,,$};
sis a signal in(or a mathematical expression over the signals in(
1
undershoots

18. SB-TemPsy-DSL
!18
Propertyq::=q1andq2|q2orq1|notq|sc
Scope sc::=globallyp|beforetp|aftertp|attp|beforep1p
afterp1p|betweent1andt2p|betweenp1andp2p
Patternp::=assertc|sbecomes⇠v|ifp1then[withinùût]p2|
existsspikeins[with[width⇠v1][amplitude⇠v2]]|
existoscillationsins[with[p2pAmp⇠v1][period⇠v2]]|
srises[monotonically]reachingv|
sfalls[monotonically]reachingv|
sovershoots[monotonically]v1byv2|
sundershoots[monotonically]v1byv2
ùû::=exactly|at most|at least
Conditionc::=c1andc2|c1orc2|notc|s⇠v
t,t1,t22R;v,v1,v22R;⇠2{<,>,=,<,,$};
sis a signal in(or a mathematical expression over the signals in(
1
Scope

19. !19
Informal Semantics:
Oscillations
•“The velocity of the satellite along the X-axis shall oscillate with
a maximum amplitude of 8000 km/h and a maximum period of
180 min”
3060120180240320400
2k
4k
6k
8k
10k
12k
p2pAmp
period
X-axis
time (min)
signal value

20. Predicate Mathematical Formulation Description
uni_m_max(¯c,B,C, [C;,CD]) 5?(C,s)=Gand8C12[C;,CD],5?(C1,s)<Gand
8C1,C22[C;,C],ifC1<C2then5?(C1,s)5?(C2,s)and
8C1,C22[C;,C],ifC1<C2then5?(C1,s)$5?(C2,s)
The valueGof signalBat time instantCis the minimum value assigned
toBwithin the interval[C;,CD]. Furthermore, the value ofGchanges
according to a unimodal function, i.e., for every time instant in[C;,C]
the value ofBis monotonically increasing and for every time instant
in[C,CD]the value ofBis monotonically decreasing.
uni_sm_max(¯c,B,C, [C;,CD]) 5?(C,s)=Gand8C12[C;,CD],5?(C1,s)<Gand
8C1,C22[C;,C],ifC1<C2then5?(C1,s)<5?(C2,s)and
8C1,C22[C;,C],ifC1<C2then5?(C1,s)>5?(C2,s)
As above, except that for every time instant in[C;,C]the value of
Bisstrictlymonotonically increasing and for every time instant in
[C,CD]the value ofBisstrictlymonotonically decreasing.
Property
¯c|=sc,¯c,[C1,C<]|=sc
Condition
¯c,C|=s⇠v,5?(C,B)⇠v
¯c|=q1andq2,(¯c|=q1)and(¯c|=q2) ¯c,C|=c1andc2,(¯c,C|=c1)and(¯c,C|=c2)
¯c|=q1orq2,(¯c|=q1)or(¯c|=q2) ¯c,C|=c1orc2,(¯c,C|=c1)or(¯c,C|=c2)
¯c|=notq,(¯c6|=q) ¯c,C|=notc,(¯c,C6|=c)
Absolute
Scope
¯c,[C;,CD]|=globallyp,¯c,[C;,CD]|=p
Event
Scope
¯c,[C;,CD]|=beforep
1
p,8C1,C2,C;<C1<C2CD,¯c,[C1,C2]|=p
1
¯c,[C;,CD]|=beforetp,C;tCDand¯c,[C;,t]|=p and9C3,C4,C;<C3<C4<C1,¯c,[C3,C4]|=p
¯c,[C;,CD]|=aftertp,C;tCDand¯c,[t,CD]|=p ¯c,[C;,CD]|=afterp
1
p,8C1,C2,C;<C1<C2CD,¯c,[C1,C2]|=p
1
¯c,[C;,CD]|=betweennandmp,C;n<mCD and9C3,C4,C2<C3<C4<CD,¯c,[C3,C4]|=p
and¯c,[n,m]|=p ¯c,[C;,CD]|=betweenp
1
andp
2
p,8C1,C2,C3,C4,C;C1<C2<C3<C4CD,
¯c,[C;,CD]|=attp,9C:C;tCDand¯c,[t,t]|=p
!
¯c,[C1,C2]|=p
1
and[C3,C4]|=p
2
"
)¯c,[C2,C3]|=p
Data Assertion
Pattern
¯c,[C;,CD]|=assertc,8C2[C;,CD],(¯c,C|=c)
¯c,[C;,CD]|=sbecomes⇠v,9C2(C;,CD],
!
5?(C,s)⇠vand8C12(C;,C),
!
5?(C1,s)⌧v

Spike
Pattern
¯c,[C;,CD]|=existsspikeins
⇥
with[width⇠v1]V[amplitude⇠v2]W
⇤
U
,9C1,C2,C32[C;,CD],C1<C2<C3,
⇣
(uni_m_min(¯c,B,C 1,[C;,C2])anduni_sm_max(¯c,B,C 2,[C1,C3])anduni_m_min(¯c,B,C 3,[C2,CD]))or
(uni_m_max(¯c,B,C 1,[C;,C2])anduni_sm_min(¯c,B,C 2,[C1,C3])anduni_m_max(¯c,B,C 3,[C2,CD]))
h
[and|C3*C1|⇠v1]
V
⇥
andmax
!'
'
5?(C1,s)*5?(C2,s)
'
'
,
'
'
5?(C2,s)*5?(C3,s)
'
'
"
⇠v2
⇤
W
i
U
⌘
Oscillation
Pattern
¯c,[C;,CD]|=existoscillationsins
⇥
with[p2pAmp⇠v1]
V[period⇠v2]
W
⇤
U
,9C1,C2,C3,C4,C52[C;,CD],C1<C2<C2<C3<C4<C5,
⇣
(uni_sm_min(¯c,B,C 2,[C1,C3])anduni_sm_max(¯c,B,C 3,[C2,C4])anduni_sm_min(¯c,B,C 4,[C3,C5]))or
(uni_sm_max(¯c,B,C 2,[C1,C3])anduni_sm_min(¯c,B,C 3,[C2,C4])anduni_sm_max(¯c,B,C 4,[C3,C5]))
h
⇥
and
'
'
5?(C2,s)*5?(C3,s)
'
'
⇠v1and
'
'
5?(C3,s)*5?(C4,s
"
|⇠v1
⇤
V
[and(C4*C2)⇠v2]
W
i
U
⌘
Rise Time
Pattern
¯c,[C;,CD]|=srises[monotonically]Ureachingv,9C2(C;,CD],
⇣
5?(C,s)$vand8C12(C;,C),
!
5?(C1,s)<v
"
⇥
and8C22(C;,C),8C32(C2,C],
!
5?(C2,s)<5?(C3,s)
"⇤
U
⌘
Overshoot
Pattern
¯c,[C;,CD]|=sovershoots[monotonically]Uv1byv2,9C2(C;,CD],
⇣
5?(C,s)$v1and8C12(C,CD],
!
5?(C1,s)v1+v2
"
[and8C22(C;,C),8C32(C2,C],
!
5?(C2,s)<5?(C3,s)
"⇤
U
⌘
Order
Relationship
Pattern
¯c,[C;,CD]|=ifp
1
then[within(exactly|at most|at least)t]Up
2
,8C1,C22[C;,CD],C1<C2,
⇣
¯c,[C1,C2]|=p
1
)
9C3,C42[C2,CD],C3<C4,
!
¯c,[C3,C4]|=p
2
⇥
and(C3*C2)»ùû…t
⇤
U
"
⌘
whereùû2{exactly,at most,at least}and»ùû…is de￿ned such that»exactly…⌘‘=’,»at most…⌘‘<=’,»at least…⌘‘>=’
t,t1,t22R;v,v1,v22R;⇠2{<,>,=,<,,$};sis a signal in(or a mathematical expression over the signals in(;scis a scope;pis a pattern.
1
Details are in the paper ;-)
!20
Formal Semantics

21. SB-TemPsy-Check:
Model-driven Trace-Checking
Procedure

22. Model-driven Trace Checking
!22
Problem of checking a
temporal property on a trace
Evaluation of an OCL constraint
on an instance of the trace
meta-model
Reduction
Equivalent to
the temporal
property
Wei Dou, Domenico Bianculli, and Lionel Briand. 2017. A Model-Driven Approach to Trace Checking of
Pattern-based Temporal Properties. In Proc. MODELS2017. IEEE Computer Society, 323–333.
*
*

23. Why Model-driven
Trace Checking?
•OCL is a standardized constraint specification language
•Supported by mature constraint checking technologies
•Existing Model-driven Trace Checking approaches have
shown to be efficient
•For “simple” temporal logic properties [Dou et al.,
Models’17] and temporal properties with temporal
aggregation [Boufaied et al, ECMFA’19]
!23
Conjecture
A model-driven trace checking approach can analyze SBTPs on real
world execution traces within practical time limits

24. SB-TemPsy-Check
!24

25. Pre-processing
!25
Trace
PreProcessing
signal values are
recorded for every
simulation time
signal values are
recorded at different
simulation times
Preprocessed
Trace

26. Model-driven Trace Checking
•Two phases:
•Input preparation
•Constraint evaluation
!26

27. Input Preparation Phase (1)
!27
•Building an instance of trace meta-model from the pre-
processed trace
contains
Record
1..*
- signal ID
- Value
contains
Entry
1..*
Trace
- simulationTime

28. Input Preparation Phase (2)
!28
•Translating the SB-TemPsy-DSL property into an OCL
constraint
•A syntax-directed translation
•It covers all constructs of SB-TemPsy-DSL

29. !29
Constraint Evaluation
•Using the OCL checker to evaluate the OCL constraint on the
instance of the pre-processed trace
•It returns a Boolean verdict
•True: if the property holds on the execution trace
•False: otherwise

30. Time Complexity (1)
•The time complexity of our procedure depends on
• the size of the trace
•the OCL definitions for the different constructs of
SB-TemPsy-DSL
!30

31. •Time Complexity w.r.t trace size:
•Data Assertion: linear
•Other patterns: polynomial
!31
Time Complexity (1)

32. Evaluation

33. Evaluation
•Our evaluation focuses on two points:
•Expressiveness of SB-TemPsy-DSL (RQ1)
•Applicability of SB-TemPsy-Check in industrial settings
(RQ2)
!33

34. RQ1: Expressiveness of
SB-TemPsy-DSL
•To which extent can SB-TemPsy-DSL express requirements of
real-world, industrial CPS applications?
•How does it compare with state-of-the-art specification
languages in terms of expressiveness?
!34

35. • We defined 101 requirements in collaboration with a domain
expert of our industrial partner
• We tried to express these requirements in SB-TemPsy-DSL,
STL and SFO
!35
RQ1: Expressiveness of
SB-TemPsy-DSL

36. •SB-TemPsy-DSL: 98 out of 101 requirements
•STL: 59 requirements
•SFO: 101 requirements
!36
RQ1: Expressiveness of
SB-TemPsy-DSL

37. •Dataset: 18 traces
•Sizes range between 41K and 1.2M entries
•217 distinct combinations of traces/properties
•Comparison with the Breach tool
•State-of-the-art offline trace checking tool for STL
RQ2: SB-TemPsy-Check
Applicability
!37

38. RQ2: SB-TemPsy-Check
Applicability
!38
•87% of the runs: SBTemPsy-Check could complete within
practical time limits, with an average execution time of 48.7 s
•13% of the runs: SB-TemPsy-Check did not finish within the
timeout (120 minutes)
•“Event-based” scope
•“Order relationship between signals” pattern

39. !39
• We ran 110 common combinations of properties/traces among tools
• SB-TemPsy-Check finished within the timeout in ≈ 97% of the runs
• SB-TemPsy-Check was able to yield a verdict within 10 s in ≈ 99%
of the cases
• SB-TemPsy-Check is slower than Breach (max exec time for
Breach is 0.15 s)
• SB-TemPsy-Check supports the verification of a much larger
set of property types
RQ2: SB-TemPsy-Check
Applicability

40. Discussion (1)
•SB-TemPsy represents a viable trade-off between:
•an expressive specification language for SBTPs
•an efficient trace-checking procedure
!40

41. •SB-TemPsy-DSL comes with a performance penalty
compared to STL
•SB-TemPsy and Breach complement each other:
•Check SBTPs that can be expressed in STL with Breach
•Check more complex SBTPs with SB-TemPsy
!41
Discussion (2)

42. Summing up…

43. !43
Trace-Checking
Signal-based Temporal Properties:
A Model-Driven Approach

44. Future work
•Extending SB-TemPsy-DSL with additional constructs
•Optimizing the OCL implementation
•Providing Trace Diagnostics information
!44

45. .lu
software verification & validation
VVS
Trace-Checking
Signal-based Temporal Properties:
A Model-Driven Approach
Chaima BOUFAIED, Claudio MENGHI, Domenico BIANCULLI, Lionel BRIAND, Yago ISASI PARACHE

46. Trace-Checking
Signal-based Temporal Properties:
A Model-Driven Approach
!46