Relational Differential Dynamic Logic
195
Simulink (Mathworks, Inc.) is an industry standard in modeling hybrid systems, but unfortunately Simulink models do not come with rigorously defined semantics. Therefore, while integration with Simulink is highly desirable any quality assurance methods for hybrid systems, formal verification methods require
some work to set up the semantics for Simulink models. The recent work [12]
tackles this problem, identifying a fragment of Simulink, and devising a translator from Simulink models to dL programs. Their translation is ingenious, and
their tool is capable of proving rather complicated properties when used in combination with KeYmaera X [15].
Relational extensions of the Floyd–Hoare logic—which can be thought of as
a discrete-time version of dL—have been energetically pursued especially in the
context of differential privacy [4,2,3].
In deductive verification of hybrid systems, an approach alternative to dL
uses nonstandard analysis [23] and regards continuous dynamics as if they were
discrete due to the existence of infinitesimal elements [24,25]. The logic used in
that framework is exactly the same as the classic Floyd–Hoare logic, and the
soundness of the logic in the hybrid setting is shown by a model-theoretic result
called the transfer principle. Its tool support has been pursued as well [11].
This is not the first time that relational reasoning—in a general sense—
has been pursued in dL. Specifically, Loos and Platzer introduce the refinement
primitive β ≤ α, which asserts a refinement relation between two hybrid dynamics, meaning the set of successor states of β is included in that of α [14].
This kind of relation is inspired by the software engineering paradigm of incremental modeling (supported by languages and tools such as Event-B [1,6]); the
result is a rigorous deductive framework for refining an abstract model (with
more nondeterminism) into a more concrete one (with less nondeterminism). In
contrast, we compare one concrete model (not necessarily with nondeterminism)
with another. Thus, our notion of relational reasoning builds more on relational
extensions of the Floyd–Hoare logic [4,2,3] than on Event-B. Combining these
two orthogonal kinds of relational extensions of dL is important future work.
Organization In Section 2, we recall some basics of differential dynamic logic
dL: its syntax, semantics and some proof rules. Our main goal, relational reasoning, is formulated in Section 3, where we identify difficulties in doing so in the
original dL. In Section 4 we introduce the semantical notion of time stretching,
and turn its theory into the new synchronization rule. After introducing our
implementation in Section 5, we describe our three case studies in Section 6.
The appendix containing omitted proofs and details, the source code and the
artifact are found at http://group-mmm.org/rddl tacas 2020/.
2 Preliminaries: Syntax and Semantics of the Logic dL
We recall some of the basics of differential dynamic logic (dL). The interested
reader is referred to [19,20] for full details.
195
Simulink (Mathworks, Inc.) is an industry standard in modeling hybrid systems, but unfortunately Simulink models do not come with rigorously defined semantics. Therefore, while integration with Simulink is highly desirable any quality assurance methods for hybrid systems, formal verification methods require
some work to set up the semantics for Simulink models. The recent work [12]
tackles this problem, identifying a fragment of Simulink, and devising a translator from Simulink models to dL programs. Their translation is ingenious, and
their tool is capable of proving rather complicated properties when used in combination with KeYmaera X [15].
Relational extensions of the Floyd–Hoare logic—which can be thought of as
a discrete-time version of dL—have been energetically pursued especially in the
context of differential privacy [4,2,3].
In deductive verification of hybrid systems, an approach alternative to dL
uses nonstandard analysis [23] and regards continuous dynamics as if they were
discrete due to the existence of infinitesimal elements [24,25]. The logic used in
that framework is exactly the same as the classic Floyd–Hoare logic, and the
soundness of the logic in the hybrid setting is shown by a model-theoretic result
called the transfer principle. Its tool support has been pursued as well [11].
This is not the first time that relational reasoning—in a general sense—
has been pursued in dL. Specifically, Loos and Platzer introduce the refinement
primitive β ≤ α, which asserts a refinement relation between two hybrid dynamics, meaning the set of successor states of β is included in that of α [14].
This kind of relation is inspired by the software engineering paradigm of incremental modeling (supported by languages and tools such as Event-B [1,6]); the
result is a rigorous deductive framework for refining an abstract model (with
more nondeterminism) into a more concrete one (with less nondeterminism). In
contrast, we compare one concrete model (not necessarily with nondeterminism)
with another. Thus, our notion of relational reasoning builds more on relational
extensions of the Floyd–Hoare logic [4,2,3] than on Event-B. Combining these
two orthogonal kinds of relational extensions of dL is important future work.
Organization In Section 2, we recall some basics of differential dynamic logic
dL: its syntax, semantics and some proof rules. Our main goal, relational reasoning, is formulated in Section 3, where we identify difficulties in doing so in the
original dL. In Section 4 we introduce the semantical notion of time stretching,
and turn its theory into the new synchronization rule. After introducing our
implementation in Section 5, we describe our three case studies in Section 6.
The appendix containing omitted proofs and details, the source code and the
artifact are found at http://group-mmm.org/rddl tacas 2020/.
2 Preliminaries: Syntax and Semantics of the Logic dL
We recall some of the basics of differential dynamic logic (dL). The interested
reader is referred to [19,20] for full details.