Requirements in Cyber-Physical Systems: Specifications and Applications
briand_lionel
971 views
87 slides
Sep 23, 2021
Slide 1 of 87
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
About This Presentation
IEEE RE 2021 keynote
Slide Content
Requirements in Cyber-Physical
Systems: Specifications and
Applications
Lionel Briand
www.lbriand.info
RE 2021
Systems: Specifications and
Applications
Lionel Briand
www.lbriand.info
RE 2021
Objectives
•Requirements engineering: Challenges specific to
cyber-physical systems
•Important applications: testing, run-time verification
•Experience from industrial research projects
2
•Requirements engineering: Challenges specific to
cyber-physical systems
•Important applications: testing, run-time verification
•Experience from industrial research projects
2
Cyber-Physical Systems
•Increasingly autonomous
•ML-based, e.g., DNN in
perception layer
•Not just recommendations, act
on the physical environment
•Possible safety implications
3
•A system of collaborating computational elements controlling
physical entities
•Increasingly autonomous
•ML-based, e.g., DNN in
perception layer
•Not just recommendations, act
on the physical environment
•Possible safety implications
3
•A system of collaborating computational elements controlling
physical entities
Example CPS
•LuxSpace: A space systems integrator based in Luxembourg
•ESAIL: A satellite that collects tracking information from
vessels
4
•LuxSpace: A space systems integrator based in Luxembourg
•ESAIL: A satellite that collects tracking information from
vessels
4
Example Requirement
Whenever the satellite modeswitches
from “Idle Mode” to “Normal Mode”,
its angular rate shall reach a value lower than 1.5°/s within 10s.
Moreover, its angular rate shall stabilize around an arbitrary value c lower
than or equal to 1.5°/s.
5
Whenever the satellite modeswitches
from “Idle Mode” to “Normal Mode”,
its angular rate shall reach a value lower than 1.5°/s within 10s.
Moreover, its angular rate shall stabilize around an arbitrary value c lower
than or equal to 1.5°/s.
5
Nature of CPS Requirements
•Focused on physical properties of the “plant” (e.g.,
satellite) over time
•Capture expected physical dynamics
•How to capture them precisely enough?
6
•Focused on physical properties of the “plant” (e.g.,
satellite) over time
•Capture expected physical dynamics
•How to capture them precisely enough?
6
7
Signal-Based Temporal
Properties (SBTP)
•SBTPscharacterize the behavior
of the system when its inputs
and outputs are signals over
time
•“The velocity of the satellite
along theX-axis may oscillate
with a maximum amplitudeof
8000 km/h and a maximum
period of 180 min”
Signal-Based Temporal
Properties (SBTP)
•SBTPscharacterize the behavior
of the system when its inputs
and outputs are signals over
time
•“The velocity of the satellite
along theX-axis may oscillate
with a maximum amplitudeof
8000 km/h and a maximum
period of 180 min”
SBTPs:
Specification vs Verification
•SBTPs are a common way to specify requirements in cyber-
physical systems
•Several languages to express SBTPs (e.g., STL, STL*, SFO)
8
Expressiveness
Efficiency
Specification
Verification
Specification vs Verification
•SBTPs are a common way to specify requirements in cyber-
physical systems
•Several languages to express SBTPs (e.g., STL, STL*, SFO)
8
Expressiveness
Efficiency
Specification
Verification
Controller Requirements
and Testing
9
and Testing
9
Acknowledgements
10
Reza Matinnejad, Shiva Nejati
10
Reza Matinnejad, Shiva Nejati
Electronic Control Units (ECUs)
More functions
Comfort and variety
Safety and reliability
Faster time-to-market
Less fuel consumption
Greenhouse gas emission laws
11
More functions
Comfort and variety
Safety and reliability
Faster time-to-market
Less fuel consumption
Greenhouse gas emission laws
11
Closed-loop Controllers
Desired Value
(Setpoint)
Actual Value (feedback)
System
Output
+
-
Control
Signal
Plant
(environment)
Controller
12
Desired Value
(Setpoint)
Actual Value (feedback)
System
Output
+
-
Control
Signal
Plant
(environment)
Controller
12
Requirements and Test Objectives
Initial Desired
(ID)
Desired ValueI (input)
Actual Value (output)
Final Desired
(FD)
time
T/2 T
Smoothness
Responsiveness
Stability
13
Initial Desired
(ID)
Desired ValueI (input)
Actual Value (output)
Final Desired
(FD)
time
T/2 T
Smoothness
Responsiveness
Stability
13
System
OutputInput
Signals
Output
Signals
Controller
Plant
(environment)
14
instability
failure pattern
discontinuity
failure pattern
•Testoracles are manual (no feedback loop)
Open-loop controllers
•Requirements can be partly based on failure
patterns regarding the output signal only
OutputInput
Signals
Output
Signals
Controller
Plant
(environment)
14
instability
failure pattern
discontinuity
failure pattern
•Testoracles are manual (no feedback loop)
Open-loop controllers
•Requirements can be partly based on failure
patterns regarding the output signal only
Summary
•Automating the testing of automotive controllers was a
narrow but central problem in the CPS context
•It gave us initial insights into the importance of
defining requirements as signal properties
•But it clearly indicated to need for further, more
general investigation into CPS requirements
15
•Automating the testing of automotive controllers was a
narrow but central problem in the CPS context
•It gave us initial insights into the importance of
defining requirements as signal properties
•But it clearly indicated to need for further, more
general investigation into CPS requirements
15
A Comprehensive
Framework and Taxonomy
for Signal-Based Properties
16
Framework and Taxonomy
for Signal-Based Properties
16
Acknowledgements
17
ChaimaBOUFAIED, Maris Jukss, Domenico BIANCULLI, YagoIsasiParache
17
ChaimaBOUFAIED, Maris Jukss, Domenico BIANCULLI, YagoIsasiParache
Challenges
•Characterizing signal behavior features:Taxonomy?
•Specification of signal-based properties: language?
•Expressiveness of property specification languages
18
•Characterizing signal behavior features:Taxonomy?
•Specification of signal-based properties: language?
•Expressiveness of property specification languages
18
Goals
•Define a taxonomyofsignal-based temporal propertiesbased
on the input of LuxSpace(satellite) and an analysis of past
published studies
•Assess the expressiveness of existing formalisms with
respect to the property types identified in the taxonomy
19
•Define a taxonomyofsignal-based temporal propertiesbased
on the input of LuxSpace(satellite) and an analysis of past
published studies
•Assess the expressiveness of existing formalisms with
respect to the property types identified in the taxonomy
19
IncreasingConstantDumpingFunctionalOrder
SpikeOscillationSignals relationship
Overview of the Taxonomy
20
Data AssertionSignal Behavior
Rise timeFall timeOvershootUndershoot
Transient
Behaviors
Signal temporal property
SpikeOscillationSignals relationship
Overview of the Taxonomy
20
Data AssertionSignal Behavior
Rise timeFall timeOvershootUndershoot
Transient
Behaviors
Signal temporal property
Temporal Logics
21
•STL, STL*
•First-order temporal logic: Signal First-Order logic (SFO)
•How do they cover the taxonomy?
21
•STL, STL*
•First-order temporal logic: Signal First-Order logic (SFO)
•How do they cover the taxonomy?
Formal specification of signal-
based temporal properties
•For each property typein the taxonomy:
•We characterizethe different signal features
•We formally specify them with SFO
22
based temporal properties
•For each property typein the taxonomy:
•We characterizethe different signal features
•We formally specify them with SFO
22
Signal Behavior:
Spike (aka bump, peak, pulse)
The concept of a spike is based
on a set of features:
•max(a1, a2): amplitude of the
spike
•w: width of the entire spike
•sp1: slope of the first-half of
the spike
•sp2: slope of the second-half
of the spike
23
Spike (aka bump, peak, pulse)
The concept of a spike is based
on a set of features:
•max(a1, a2): amplitude of the
spike
•w: width of the entire spike
•sp1: slope of the first-half of
the spike
•sp2: slope of the second-half
of the spike
23
•A spike property specifies a constraint on the existence of a
spike with certain features.
•“In signal s, there is exactly one spike with a maximum width
of 20 tuand a maximum amplitude of 1”
24
Example of Spike Property
spike with certain features.
•“In signal s, there is exactly one spike with a maximum width
of 20 tuand a maximum amplitude of 1”
24
Example of Spike Property
Order relationship between
signals
“Whenever signal s1 exhibits a behavior,
signal s2 responds with another behavior”
signals
“Whenever signal s1 exhibits a behavior,
signal s2 responds with another behavior”
Example
26
“If in signal s1 there exists one spike with a
maximum width of 30 tuand a maximum amplitude
of 1, then signal s2 shall become less than 0.5
within 10 tu”
26
“If in signal s1 there exists one spike with a
maximum width of 30 tuand a maximum amplitude
of 1, then signal s2 shall become less than 0.5
within 10 tu”
Evaluation of the Property
27
“If in signal s1 there exists one spike with a
maximum width of 30 tuand a maximum amplitude
of 1, then signal s2 shall become less than 0.5
within 10 tu”
S1
S2
27
“If in signal s1 there exists one spike with a
maximum width of 30 tuand a maximum amplitude
of 1, then signal s2 shall become less than 0.5
within 10 tu”
S1
S2
Evaluation of the Property
28
“If in signal s1 there exists one spike with a
maximum width of 30 tuand a maximum amplitude
of 1, then signal s2 shall become less than 0.5
within 10 tu”
S1
S2
28
“If in signal s1 there exists one spike with a
maximum width of 30 tuand a maximum amplitude
of 1, then signal s2 shall become less than 0.5
within 10 tu”
S1
S2
Temporal Logics:Expressiveness
29
29
Summary
30
•STLhas limited expressiveness, restricting its application in practice to simple property types (e.g., data assertion), but good support from a number of tools.
•STL* is more expressive than STL provided that some assumptions (e.g., on the signal shape) are made; however, such assumptions are impractical. In addition, STL* suffers from the limited tool support.
•SFOis the most expressive language for the property types defined in our taxonomy; however, its application is challenging given the computational complexity of associated monitoring algorithms and the lack of tools.
30
•STLhas limited expressiveness, restricting its application in practice to simple property types (e.g., data assertion), but good support from a number of tools.
•STL* is more expressive than STL provided that some assumptions (e.g., on the signal shape) are made; however, such assumptions are impractical. In addition, STL* suffers from the limited tool support.
•SFOis the most expressive language for the property types defined in our taxonomy; however, its application is challenging given the computational complexity of associated monitoring algorithms and the lack of tools.
Online Testing
Acknowledgements
32
Claudio Menghi, Shiva Nejati, KhouloudGaaloul
32
Claudio Menghi, Shiva Nejati, KhouloudGaaloul
The CPS Development Workflow
Modeling
(Simulink)TestingCoding
33
Modeling
(Simulink)TestingCoding
33
Goal
Testing
Model
Requirements
Check
Requires test oracles
34
InputOutputs
Testing
Model
Requirements
Check
Requires test oracles
34
InputOutputs
Online Testing
•Test oracles should check outputs in an onlinemode
•Simulink models are often compute-intensive
•E.g., one simulationof the satellite behavior required 1.5 h
•We must stop execution as soon as a requirement is
violated
35
•Test oracles should check outputs in an onlinemode
•Simulink models are often compute-intensive
•E.g., one simulationof the satellite behavior required 1.5 h
•We must stop execution as soon as a requirement is
violated
35
•Test oracles should provide a quantitative measure of the
degree of satisfaction orviolationof a requirement
•The error after 2000sshould be lower than 2 degrees
Risk Level
36
degree of satisfaction orviolationof a requirement
•The error after 2000sshould be lower than 2 degrees
Risk Level
36
Objective
onlinemagnitude/time
continuous
signals
quantitative
satisfaction
degree
parameter
uncertainties
Automatically generate test oraclesfrom SBTPs
37
onlinemagnitude/time
continuous
signals
quantitative
satisfaction
degree
parameter
uncertainties
Automatically generate test oraclesfrom SBTPs
37
Restricted Signals
First-Order Logic (RFOL)
Online
38
Expressiveness
The First-Order Logic of Signals
A Bakhirkin, T Ferrere, TA Henzinger, D Ničkovićl
2018 International Conference on Embedded Software (EMSOFT)RFOL < SFO
First-Order Logic (RFOL)
Online
38
Expressiveness
The First-Order Logic of Signals
A Bakhirkin, T Ferrere, TA Henzinger, D Ničkovićl
2018 International Conference on Embedded Software (EMSOFT)RFOL < SFO
Restricted Signals
First-Order Logic (RFOL)
39
Example restriction
Two free time variables t and t’, two segments of signal f, f(t) and
f(t’) cannot be simultaneously computed during online checking
The difference among the satellite realattitude and the target
attitude after 2000sshould not be above 2 degrees
Syntax
First-Order Logic (RFOL)
39
Example restriction
Two free time variables t and t’, two segments of signal f, f(t) and
f(t’) cannot be simultaneously computed during online checking
The difference among the satellite realattitude and the target
attitude after 2000sshould not be above 2 degrees
Syntax
Restricted Signals
First-Order Logic (RFOL)
Semantics
The evaluation of the formula is
•a fitness value in the range [−1, 1]. (risk level)
•A value in [0, 1]indicates that the formula holds
•A value in [−1, 0) indicates that the formula is violated
40
First-Order Logic (RFOL)
Semantics
The evaluation of the formula is
•a fitness value in the range [−1, 1]. (risk level)
•A value in [0, 1]indicates that the formula holds
•A value in [−1, 0) indicates that the formula is violated
40
Test Oracle Generation
41
We propose a procedure to translate RFOLinto Simulink oracles
41
We propose a procedure to translate RFOLinto Simulink oracles
Evaluating Test Oracles
42
Simulink
modelOracle
OutputsResultsInputs
•we can stopsimulations when the result is below a threshold
after the simulation time exceeds a given value
42
Simulink
modelOracle
OutputsResultsInputs
•we can stopsimulations when the result is below a threshold
after the simulation time exceeds a given value
RFOL Expressiveness
•11 case studies from 2 industry partners
•LuxSpacea satellite company
•QRACorpa verification tool vendor
•98 requirements
43
RFOL is sufficiently expressive to capture
all the 98 requirements
•11 case studies from 2 industry partners
•LuxSpacea satellite company
•QRACorpa verification tool vendor
•98 requirements
43
RFOL is sufficiently expressive to capture
all the 98 requirements
For compute-intensive industrial models,
our oracles introduce very little time overhead (6%)
but
save a great deal of time when they identify failures (96%)
Benefits from Online Test Oracles
44
our oracles introduce very little time overhead (6%)
but
save a great deal of time when they identify failures (96%)
Benefits from Online Test Oracles
44
Trace CheckingSBTPs
Acknowledgements
46
ChaimaBOUFAIED, Claudio MENGHI, Domenico BIANCULLI, YagoISASI PARACHE
46
ChaimaBOUFAIED, Claudio MENGHI, Domenico BIANCULLI, YagoISASI PARACHE
Trace Checking
47
Execution trace
…
System requirements
SBTPs
Trace
Checking
System
Trace Checking is crucial in a CPS context
47
Execution trace
…
System requirements
SBTPs
Trace
Checking
System
Trace Checking is crucial in a CPS context
•Building a Domain-Specific Language (DSL)for specifying
signal-based properties
•Developing efficient, scalable trace checking and monitoring
algorithms
Main Goals
48
signal-based properties
•Developing efficient, scalable trace checking and monitoring
algorithms
Main Goals
48
SB-TemPsy-DSL
•Pattern-basedspecification language
•Supports the common types of SBTPsidentified in the
taxonomy
•Focus on usability
49
•Pattern-basedspecification language
•Supports the common types of SBTPsidentified in the
taxonomy
•Focus on usability
49
Specification Language
50
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)
•Its syntaxis close to natural language
•It does not require a strong mathematical background
•Important for adoption among practitioners
50
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)
•Its syntaxis close to natural language
•It does not require a strong mathematical background
•Important for adoption among practitioners
SB-TemPsyDSL
51
existoscillationsinX-axis
withp2pAmp<=8000
withperiod<=180
•“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”
51
existoscillationsinX-axis
withp2pAmp<=8000
withperiod<=180
•“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”
•Building a DSL for specifying signal-based properties
•Developing efficient, scalable trace checking and monitoring
algorithms
Main Goals
52
•Developing efficient, scalable trace checking and monitoring
algorithms
Main Goals
52
SB-TemPsy-Check
53
53
54
Eclipse OCL
Trace
SB-TemPsy-
Property
Trace
instance
TemPsyExpression
instance
OCL constraints
on Traceclass
TemPsy-Check
Model-driven Offline Trace
Checking
Eclipse OCL
Trace
SB-TemPsy-
Property
Trace
instance
TemPsyExpression
instance
OCL constraints
on Traceclass
TemPsy-Check
Model-driven Offline Trace
Checking
Evaluation
•Our evaluation focuses on two points:
•Expressiveness of SB-TemPsy-DSL(RQ1)
•Applicability of SB-TemPsy-Checkin industrial settings
(RQ2)
55
•Our evaluation focuses on two points:
•Expressiveness of SB-TemPsy-DSL(RQ1)
•Applicability of SB-TemPsy-Checkin industrial settings
(RQ2)
55
RQ1: Expressiveness of
SB-TemPsy-DSL
•To which extent can SB-TemPsy-DSL express requirements of
real-world, industrial CPS applications?
•How does it comparewith state-of-the-art specification
languages in terms ofexpressiveness?
56
SB-TemPsy-DSL
•To which extent can SB-TemPsy-DSL express requirements of
real-world, industrial CPS applications?
•How does it comparewith state-of-the-art specification
languages in terms ofexpressiveness?
56
•We defined 101requirements in collaboration with a domain
expert
•We tried to expressthese requirements in SB-TemPsy-DSL,
STLand SFO
57
RQ1: Expressiveness of
SB-TemPsy-DSL
expert
•We tried to expressthese requirements in SB-TemPsy-DSL,
STLand SFO
57
RQ1: Expressiveness of
SB-TemPsy-DSL
•SB-TemPsy-DSL: 98 out of 101requirements
•STL: 59requirements
•SFO: 101requirements
58
RQ1: Expressiveness of
SB-TemPsy-DSL
•STL: 59requirements
•SFO: 101requirements
58
RQ1: Expressiveness of
SB-TemPsy-DSL
59
•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
RQ2: SB-TemPsy-Check
Applicability
•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
RQ2: SB-TemPsy-Check
Applicability
60
RQ2: SB-TemPsy-Check
Applicability
•Among110combinations of properties/traces that are
common among tools:
•SB-TemPsy-Check
•is slowerthan Breach
•but it supports the verification of a much larger set of
property types
RQ2: SB-TemPsy-Check
Applicability
•Among110combinations of properties/traces that are
common among tools:
•SB-TemPsy-Check
•is slowerthan Breach
•but it supports the verification of a much larger set of
property types
Discussion (1)
•SB-TemPsyrepresents a viabletrade-off between:
•an expressivespecification language for SBTPs
•an efficienttrace-checking procedure
61
•SB-TemPsyrepresents a viabletrade-off between:
•an expressivespecification language for SBTPs
•an efficienttrace-checking procedure
61
•SB-TemPsy-DSL comes with a performance penalty
compared to STL
•SB-TemPsyand Breach complementeach other:
•Check SBTPs that can be expressed in STL with
Breach
•Check more complex SBTPs with SB-TemPsy
62
Discussion (2)
compared to STL
•SB-TemPsyand Breach complementeach other:
•Check SBTPs that can be expressed in STL with
Breach
•Check more complex SBTPs with SB-TemPsy
62
Discussion (2)
Hybrid Logic of Signals
63
63
Acknowledgements
64
Claudio Menghi, Enrico Viganò, Domenico Bianculli
64
Claudio Menghi, Enrico Viganò, Domenico Bianculli
•Pattern-based languages are by definition limited
•More expressive language, less restricted
•Not pattern-based, but a dedicated temporal logic
•Rely on off-the-shelf SMT solvers for trace checking
65
Motivations
•More expressive language, less restricted
•Not pattern-based, but a dedicated temporal logic
•Rely on off-the-shelf SMT solvers for trace checking
65
Motivations
66
Anatomy of Requirements
Whenever the satellite mode switches from “Idle Mode” to “Normal Mode”,
the angular rate shall reach a value lower than 1.5°/s within 10s.
Moreover, the angular rate shall stabilize around an arbitrary value clower than or equal to 1.5°/s.
Indices -Software behavior
Trace
Anatomy of Requirements
Whenever the satellite mode switches from “Idle Mode” to “Normal Mode”,
the angular rate shall reach a value lower than 1.5°/s within 10s.
Moreover, the angular rate shall stabilize around an arbitrary value clower than or equal to 1.5°/s.
Indices -Software behavior
Trace
67
Anatomy of Requirements
Whenever the satellite mode switches from “Idle Mode” to “Normal Mode”,
the angular rate shall reach a value lower than 1.5°/s within 10s.
Moreover, the angular rate shall stabilize around an arbitrary value clower than or equal to 1.5°/s.
Indices -Software behavior
Timestamps -Physical behaviour
10s
Trace
Anatomy of Requirements
Whenever the satellite mode switches from “Idle Mode” to “Normal Mode”,
the angular rate shall reach a value lower than 1.5°/s within 10s.
Moreover, the angular rate shall stabilize around an arbitrary value clower than or equal to 1.5°/s.
Indices -Software behavior
Timestamps -Physical behaviour
10s
Trace
68
Anatomy of Requirements
Whenever the satellite mode switches from “Idle Mode” to “Normal Mode”,
the angular rate shall reach a value lower than 1.5°/s within 10s.
Moreover, the angular rate shall stabilize around an arbitrary value clower than or equal to 1.5°/s.
Indices -Software behavior
Timestamps -Physical behaviourReal-valued variables
Trace
Anatomy of Requirements
Whenever the satellite mode switches from “Idle Mode” to “Normal Mode”,
the angular rate shall reach a value lower than 1.5°/s within 10s.
Moreover, the angular rate shall stabilize around an arbitrary value clower than or equal to 1.5°/s.
Indices -Software behavior
Timestamps -Physical behaviourReal-valued variables
Trace
Language Objective
•We designed HLS, a language for specifying CPS properties
that seamlessly combine the features of sequence based (e.g.,
STL) and time-based languages (e.g., LTL).
69
•We designed HLS, a language for specifying CPS properties
that seamlessly combine the features of sequence based (e.g.,
STL) and time-based languages (e.g., LTL).
69
70
Expressing CPS Requirements
exists !such that (!<1.5 and
forallσ0in [0;5] such that
((mode @iσ0) = 0 and (mode @i(σ0+ 1)) = 3)
implies
exists τ0in [0s;10s] such that
(ang-rate @t (τ0+ i2t(σ0)) < !)))
HLS allows using existentialand universalquantifierswith
Expressing CPS Requirements
exists !such that (!<1.5 and
forallσ0in [0;5] such that
((mode @iσ0) = 0 and (mode @i(σ0+ 1)) = 3)
implies
exists τ0in [0s;10s] such that
(ang-rate @t (τ0+ i2t(σ0)) < !)))
HLS allows using existentialand universalquantifierswith
71
Expressing CPS Requirements
exists !such that (!<1.5 and
forall σ0in [0;5] such that
((mode @i σ0) = 0 and (mode @i (σ0+ 1)) = 3)
implies
exists τ0in [0s;10s] such that
(ang-rate @t (τ0+ i2t(σ0)) < !)))
HLS allows using existentialand universalquantifierswith
•timestamp variables
Expressing CPS Requirements
exists !such that (!<1.5 and
forall σ0in [0;5] such that
((mode @i σ0) = 0 and (mode @i (σ0+ 1)) = 3)
implies
exists τ0in [0s;10s] such that
(ang-rate @t (τ0+ i2t(σ0)) < !)))
HLS allows using existentialand universalquantifierswith
•timestamp variables
72
Expressing CPS Requirements
exists !such that (!<1.5 and
forall σ0in [0;5] such that
((mode @i σ0) = 0 and (mode @i (σ0+ 1)) = 3)
implies
exists τ0in [0s;10s] such that
(ang-rate @t (τ0+ i2t(σ0)) < !)))
HLS allows using existentialand universalquantifierswith
•timestamp variables
•index variables
Expressing CPS Requirements
exists !such that (!<1.5 and
forall σ0in [0;5] such that
((mode @i σ0) = 0 and (mode @i (σ0+ 1)) = 3)
implies
exists τ0in [0s;10s] such that
(ang-rate @t (τ0+ i2t(σ0)) < !)))
HLS allows using existentialand universalquantifierswith
•timestamp variables
•index variables
73
Expressing CPS Requirements
exists !such that (!<1.5 and
forall σ0in [0;5] such that
((mode @i σ0) = 0 and (mode @i (σ0+ 1)) = 3)
implies
exists τ0in [0s;10s] such that
(ang-rate @t (τ0+ i2t(σ0)) < !)))
HLS allows using existentialand universalquantifierswith
•timestamp variables
•index variables
•real-valued variables
Expressing CPS Requirements
exists !such that (!<1.5 and
forall σ0in [0;5] such that
((mode @i σ0) = 0 and (mode @i (σ0+ 1)) = 3)
implies
exists τ0in [0s;10s] such that
(ang-rate @t (τ0+ i2t(σ0)) < !)))
HLS allows using existentialand universalquantifierswith
•timestamp variables
•index variables
•real-valued variables
74
Expressing CPS Requirements
exists !such that (!<1.5 and
forall σ0in [0;5] such that
((mode @i σ0) = 0 and (mode @i (σ0+ 1)) = 3)
implies
exists τ0in [0s;10s] such that
(ang-rate @t (τ0+ i2t(σ0)) < !)))
HLS allows using existentialand universalquantifierswith
•timestamp variables
•index variables
•real-valued variables
HLS supports specifications that use
Expressing CPS Requirements
exists !such that (!<1.5 and
forall σ0in [0;5] such that
((mode @i σ0) = 0 and (mode @i (σ0+ 1)) = 3)
implies
exists τ0in [0s;10s] such that
(ang-rate @t (τ0+ i2t(σ0)) < !)))
HLS allows using existentialand universalquantifierswith
•timestamp variables
•index variables
•real-valued variables
HLS supports specifications that use
75
Expressing CPS Requirements
exists !such that (!<1.5 and
forall σ0in [0;5] such that
((mode @i σ0) = 0 and (mode @i (σ0+ 1)) = 3)
implies
exists τ0in [0s;10s] such that
(ang-rate @t (τ0+ i2t(σ0)) < !)))
HLS allows using existentialand universalquantifierswith
•timestamp variables
•index variables
•real-valued variables
HLS supports specifications that use
•a signal ata certain timestamp
Expressing CPS Requirements
exists !such that (!<1.5 and
forall σ0in [0;5] such that
((mode @i σ0) = 0 and (mode @i (σ0+ 1)) = 3)
implies
exists τ0in [0s;10s] such that
(ang-rate @t (τ0+ i2t(σ0)) < !)))
HLS allows using existentialand universalquantifierswith
•timestamp variables
•index variables
•real-valued variables
HLS supports specifications that use
•a signal ata certain timestamp
76
Expressing CPS Requirements
exists !such that (!<1.5 and
forallσ0in [0;5] such that
((mode @iσ0) = 0 and (mode @i(σ0+ 1)) = 3)
implies
exists τ0in [0s;10s] such that
(ang-rate @t (τ0+ i2t(σ0)) < !)))
HLS allows using existentialand universalquantifierswith
•timestamp variables
•index variables
•real-valued variables
HLS supports specifications that use
•a signal ata certain timestamp
•a signal ata certain index
Expressing CPS Requirements
exists !such that (!<1.5 and
forallσ0in [0;5] such that
((mode @iσ0) = 0 and (mode @i(σ0+ 1)) = 3)
implies
exists τ0in [0s;10s] such that
(ang-rate @t (τ0+ i2t(σ0)) < !)))
HLS allows using existentialand universalquantifierswith
•timestamp variables
•index variables
•real-valued variables
HLS supports specifications that use
•a signal ata certain timestamp
•a signal ata certain index
77
Expressing CPS Requirements
exists !such that (!<1.5 and
forall σ0in [0;5] such that
((mode @i σ0) = 0 and (mode @i (σ0+ 1)) = 3)
implies
exists τ0in [0s;10s] such that
(ang-rate @t (τ0+ i2t(σ0)) < !)))
HLS allows using existentialand universalquantifierswith
•timestamp variables
•index variables
•real-valued variables
HLS supports specifications that use
•a signal ata certain timestamp
•a signal ata certain index
•the timestampof an index(and vice versa)
Expressing CPS Requirements
exists !such that (!<1.5 and
forall σ0in [0;5] such that
((mode @i σ0) = 0 and (mode @i (σ0+ 1)) = 3)
implies
exists τ0in [0s;10s] such that
(ang-rate @t (τ0+ i2t(σ0)) < !)))
HLS allows using existentialand universalquantifierswith
•timestamp variables
•index variables
•real-valued variables
HLS supports specifications that use
•a signal ata certain timestamp
•a signal ata certain index
•the timestampof an index(and vice versa)
78
Expressing CPS Requirements
HLS allows using existentialand universalquantifierswith
•timestamp variables
•index variables
•real-valued variables
HLS supports specifications that use
•a signal ata certain timestamp
•a signal ata certain index
•the timestampof an index(and vice versa)
•expressionscombining timestamps, indices, and real-valuedvariables
exists !such that (!<1.5 and
forall σ0in [0;5] such that
((mode @i σ0) = 0 and (mode @i (σ0+ 1)) = 3)
implies
exists τ0in [0s;10s] such that
(ang-rate @t (τ0+ i2t(σ0)) < !)))
Expressing CPS Requirements
HLS allows using existentialand universalquantifierswith
•timestamp variables
•index variables
•real-valued variables
HLS supports specifications that use
•a signal ata certain timestamp
•a signal ata certain index
•the timestampof an index(and vice versa)
•expressionscombining timestamps, indices, and real-valuedvariables
exists !such that (!<1.5 and
forall σ0in [0;5] such that
((mode @i σ0) = 0 and (mode @i (σ0+ 1)) = 3)
implies
exists τ0in [0s;10s] such that
(ang-rate @t (τ0+ i2t(σ0)) < !)))
Logic-based TracEcheckErfor HLS
•ThEodorE:
•Reducestrace-checking problem to a SMTproblem
•Allows the use of efficient off-the-shelfSMT solvers
79
•ThEodorE:
•Reducestrace-checking problem to a SMTproblem
•Allows the use of efficient off-the-shelfSMT solvers
79
Expressiveness
80
HLScould express allthe requirements
of our case study, many more than
SB-TemPsy-DSL (+31%) and STL (+51%).
80
HLScould express allthe requirements
of our case study, many more than
SB-TemPsy-DSL (+31%) and STL (+51%).
Applicability
81
ThEodorEcomputed a verdict for 74.5%of trace-
requirementcombinations.
ThEodorEproduced a verdict for 67.9%of the 337
trace-requirement combinations that could not be
checked by the other tools.
81
ThEodorEcomputed a verdict for 74.5%of trace-
requirementcombinations.
ThEodorEproduced a verdict for 67.9%of the 337
trace-requirement combinations that could not be
checked by the other tools.
Other Topics and Conclusions
Other Topics
•Understand requirement violations
•Determine assumptions that must be met to satisfy
requirements
•Usability of specification languages
83
•Understand requirement violations
•Determine assumptions that must be met to satisfy
requirements
•Usability of specification languages
83
Conclusions
•Expressing and using requirements in cyber-physical
systems requires trade-offs between several factors
•Expressiveness: What types of properties need to be
captured
•Style: Pattern-based (e.g., DSL) vs low-level abstraction (e.g.,
temporal logic)
•Usability<> expressiveness
84
•Expressing and using requirements in cyber-physical
systems requires trade-offs between several factors
•Expressiveness: What types of properties need to be
captured
•Style: Pattern-based (e.g., DSL) vs low-level abstraction (e.g.,
temporal logic)
•Usability<> expressiveness
84
Conclusions
•Required trace checking performance(trace sizes ...)
•Offine versus online analysis
•Further systematic investigation into trade-offs is required
•Engineers need to know what is their best options based
on the above factors
•Though there is active research on languages and
automation, there is little going on regarding trade-offs
85
•Required trace checking performance(trace sizes ...)
•Offine versus online analysis
•Further systematic investigation into trade-offs is required
•Engineers need to know what is their best options based
on the above factors
•Though there is active research on languages and
automation, there is little going on regarding trade-offs
85
Selected References
•Reza Matinnejad, Shiva Nejati, Lionel Briand, Thomas Bruckmann, “Search-based automated testing of continuous
controllers: Framework, tool support, and case studies”, Information and Software Technology (Elsevier), 2015
•Reza Matinnejad, Shiva Nejati, Lionel Briand, Thomas Bruckmann, “Test Generation and Test Prioritization for Simulink
Models with Dynamic Behavior”, IEEE Transactions on Software Engineering, 2018
•Claudio Menghi, Shiva Nejati, KhouloudGaaloul, Lionel Briand, “Generating Automated and Online Test Oracles for
Simulink Models with Continuous and Uncertain Behaviors”, ACM ESEC/FSE 2019
•ChaimaBoufaied, Maris Jukss, Domenico Bianculli, Lionel Briand, YagoIsasiParache, “Signal-Based Properties of
Cuber-Physical Systems: Taxonomy and Logic-based Characterisation”, Journal of Systems and Software (Elsevier),
2020
•ChaimaBoufaied, Claudio Menghi, Domenico Bianculli, Lionel Briand, YagoIsasiParache, “Trace-Checking Signal-
based Temporal Properties: A Model-Driven Approach”, IEEE/ACM ASE 2020
•Claudio Menghi, Enrico Viganò, Domenico Bianculli, Lionel Briand, “Trace-Checking CPS Properties: Bridging the
Cyber-Physical Gap”, IEEE/ACM ICSE 2021
86
•Reza Matinnejad, Shiva Nejati, Lionel Briand, Thomas Bruckmann, “Search-based automated testing of continuous
controllers: Framework, tool support, and case studies”, Information and Software Technology (Elsevier), 2015
•Reza Matinnejad, Shiva Nejati, Lionel Briand, Thomas Bruckmann, “Test Generation and Test Prioritization for Simulink
Models with Dynamic Behavior”, IEEE Transactions on Software Engineering, 2018
•Claudio Menghi, Shiva Nejati, KhouloudGaaloul, Lionel Briand, “Generating Automated and Online Test Oracles for
Simulink Models with Continuous and Uncertain Behaviors”, ACM ESEC/FSE 2019
•ChaimaBoufaied, Maris Jukss, Domenico Bianculli, Lionel Briand, YagoIsasiParache, “Signal-Based Properties of
Cuber-Physical Systems: Taxonomy and Logic-based Characterisation”, Journal of Systems and Software (Elsevier),
2020
•ChaimaBoufaied, Claudio Menghi, Domenico Bianculli, Lionel Briand, YagoIsasiParache, “Trace-Checking Signal-
based Temporal Properties: A Model-Driven Approach”, IEEE/ACM ASE 2020
•Claudio Menghi, Enrico Viganò, Domenico Bianculli, Lionel Briand, “Trace-Checking CPS Properties: Bridging the
Cyber-Physical Gap”, IEEE/ACM ICSE 2021
86
Requirements in Cyber-Physical
Systems: Specifications and
Applications
Lionel Briand
www.lbriand.info
RE 2021
Systems: Specifications and
Applications
Lionel Briand
www.lbriand.info
RE 2021
Tags
Categories
GeneralDownload
Download Slideshow Get the original presentation fileQuick Actions
Statistics
- Views 971
- Slides 87
- Favorites 1
- Age 1536 days
Related Slideshows
22
Pray For The Peace Of Jerusalem and You Will Prosper
RodolfoMoralesMarcuc
34 views
26
Don_t_Waste_Your_Life_God.....powerpoint
chalobrido8
37 views
31
VILLASUR_FACTORS_TO_CONSIDER_IN_PLATING_SALAD_10-13.pdf
JaiJai148317
34 views
14
Fertility awareness methods for women in the society
Isaiah47
31 views
35
Chapter 5 Arithmetic Functions Computer Organisation and Architecture
RitikSharma297999
30 views
5
syakira bhasa inggris (1) (1).pptx.......
ourcommunity56
31 views