194
J. Kolˇ c´ ak et al.
we call the synchronization rule, generalizes the kind of reasoning in Example 1
using the notion of time stretching.
Technical Contributions We make the following technical contributions.
1. Formulation of relational reasoning in dL. We find that relational properties are expressible in dL, using disjoint variables in a sequential composition. This representation, however, does not allow the use of the rich logical
infrastructure of dL (such as the (DI) rule).
2. Time stretching, semantically and syntactically. To alleviate this difficulty, we first develop the theory of time stretching, so that we can compare
two dynamics at different timepoints (cf. Example 1). Accommodating this
semantical notion in dL and KeYmaera X is not possible per se. We introduce an indirect syntactic alternative, which turns out to be better suited
in fact to many case studies (where we compare the two dynamics at the
same “position,” much like in Example 1). The resulting synchronization
rule in dL has a clean presentation (Theorem 24), owing to the syntactic Lie
derivative operator in dL.
3. Implementation and case studies. We implemented the new synchronization rule as an extension of KeYmaera X. We used it successfully for
establishing nontrivial relational properties in case studies taken from the
automotive domain.
Relational Reasoning in Practice We contend relational reasoning has
practical significance based on our collaboration with an industry partner. Relational properties, especially with an aspect of monotonicity, abound in real-world
examples. In particular, we have often encountered situations where we have a
parametrized model M (p) and need to show a property of the form:
p 1 < p 2 implies M (p 2 ) is less safe than M (p 1 ).
(2)
These properties occur especially in the context of product lines, where the same
model can come in many slight variants. Example 1 is such a situation.
Relational statements (such as monotonicity) are easy to state and interpret.
Intuitions about the direction of the change in a behavior of a system resulting
from the change of a parameter are more often valid than intuitions about the
amount of such a change. These kinds of simple statements are often used by
engineers to establish the basic credibility of a model. Qualitative, relational
properties also tend to be easier to prove than exact, quantitative properties.
Finally, monotonicity can serve as a powerful technique in test-case reduction.
If a safety property is too complex to be deductively verified, one usually turns
to testing. It is often still possible to establish a simple monotonicity property of
the form (2). This can powerfully boost testing efforts: one can focus exclusively
on establishing safety for the extreme case M (p max ).
Related Work Since this work is about its relational extension, the works
we mentioned on dL are naturally relevant. We discuss other related works here.
J. Kolˇ c´ ak et al.
we call the synchronization rule, generalizes the kind of reasoning in Example 1
using the notion of time stretching.
Technical Contributions We make the following technical contributions.
1. Formulation of relational reasoning in dL. We find that relational properties are expressible in dL, using disjoint variables in a sequential composition. This representation, however, does not allow the use of the rich logical
infrastructure of dL (such as the (DI) rule).
2. Time stretching, semantically and syntactically. To alleviate this difficulty, we first develop the theory of time stretching, so that we can compare
two dynamics at different timepoints (cf. Example 1). Accommodating this
semantical notion in dL and KeYmaera X is not possible per se. We introduce an indirect syntactic alternative, which turns out to be better suited
in fact to many case studies (where we compare the two dynamics at the
same “position,” much like in Example 1). The resulting synchronization
rule in dL has a clean presentation (Theorem 24), owing to the syntactic Lie
derivative operator in dL.
3. Implementation and case studies. We implemented the new synchronization rule as an extension of KeYmaera X. We used it successfully for
establishing nontrivial relational properties in case studies taken from the
automotive domain.
Relational Reasoning in Practice We contend relational reasoning has
practical significance based on our collaboration with an industry partner. Relational properties, especially with an aspect of monotonicity, abound in real-world
examples. In particular, we have often encountered situations where we have a
parametrized model M (p) and need to show a property of the form:
p 1 < p 2 implies M (p 2 ) is less safe than M (p 1 ).
(2)
These properties occur especially in the context of product lines, where the same
model can come in many slight variants. Example 1 is such a situation.
Relational statements (such as monotonicity) are easy to state and interpret.
Intuitions about the direction of the change in a behavior of a system resulting
from the change of a parameter are more often valid than intuitions about the
amount of such a change. These kinds of simple statements are often used by
engineers to establish the basic credibility of a model. Qualitative, relational
properties also tend to be easier to prove than exact, quantitative properties.
Finally, monotonicity can serve as a powerful technique in test-case reduction.
If a safety property is too complex to be deductively verified, one usually turns
to testing. It is often still possible to establish a simple monotonicity property of
the form (2). This can powerfully boost testing efforts: one can focus exclusively
on establishing safety for the extreme case M (p max ).
Related Work Since this work is about its relational extension, the works
we mentioned on dL are naturally relevant. We discuss other related works here.