192 lines
8 KiB
Typst
192 lines
8 KiB
Typst
#import "@preview/cetz:0.4.0"
|
|
#import "@preview/finite:0.4.1"
|
|
|
|
#set page(paper: "a4")
|
|
#set par(justify: true)
|
|
#set raw(syntaxes: "zelus.sublime-syntax")
|
|
#show raw: set text(font: "CaskaydiaCove NF")
|
|
|
|
#let lustre = smallcaps[Lustre]
|
|
#let esterel = smallcaps[Esterel]
|
|
#let simulink = smallcaps[Simulink]
|
|
#let sundials = smallcaps[Sundials CVODE]
|
|
#let zelus = smallcaps[Zélus]
|
|
#let TODO(..what) = {
|
|
let msg = if what.pos().len() == 0 { "" } else { ": " + what.pos().join("") }
|
|
block(fill: red, width: 100%, inset: 5pt, align(center, raw("TODO" + msg)))
|
|
}
|
|
#let adot(s) = $accent(#s, dot)$
|
|
#let addot(s) = $accent(#s, dot.double)$
|
|
|
|
#align(center)[
|
|
#text(16pt)[
|
|
*Internship Report --- MPRI M2 \
|
|
Hybrid System Models with Transparent Assertions*
|
|
]
|
|
|
|
Henri Saudubray, supervised by Marc Pouzet, Inria PARKAS
|
|
]\
|
|
|
|
#heading(outlined: false)[General Context]
|
|
What is the report about? Where does the problem come from? What is the state of
|
|
the art in that area?
|
|
|
|
Hybrid systems modelers such as #simulink are essential tools in the development
|
|
of embedded systems evolving in physical environments. They allow for precise
|
|
descriptions of hybrid systems through both continuous-time behaviour defined
|
|
through Ordinary Differential Equations (ODEs) and discrete-time reactive
|
|
behaviour similar to what is found in the synchronous languages such as #lustre.
|
|
The #zelus language aims to reconcile synchronous languages with hybrid systems,
|
|
by taking a synchronous language kernel and extending it with continuous-time
|
|
constructs similar to what is found in tools like #simulink. Continuous-time
|
|
behaviour is computed through the use of an off-the-shelf ODE solver such as
|
|
#sundials.
|
|
|
|
#heading(outlined: false)[Research Problem]
|
|
What specific question(s) have you studied? What motivates the question? What
|
|
are the applications/consequences? Is it a new problem? Why did you choose this
|
|
problem?
|
|
|
|
The simulation of hybrid system models, as done in #simulink and #zelus, uses a
|
|
single ODE solver instance to simulate the entire model. This has various
|
|
advantages: it is less computationally intensive, and simplifies the work of the
|
|
compiler. Unfortunately, it also raises a difficult problem: sub-systems which
|
|
seemingly should not interfere with each other end up affecting each other's
|
|
results. This is due to the chosen integration method: an adaptive solver like
|
|
#sundials will vary its step length throughout the integration process, and the
|
|
addition of ODEs in the overall system can influence these step lengths,
|
|
affecting the results obtained for pre-existing ODEs. This is particularly
|
|
problematic in the case of runtime assertions, which are typically expected to
|
|
be transparent: they should not affect the final result of the computation.
|
|
|
|
#heading(outlined: false)[Proposed Contributions]
|
|
What is your answer to the research problem? Please remain at a high level;
|
|
technical details should be given in the main body of the report. Pay special
|
|
attention to the description of the _scientific_ approach.
|
|
|
|
To solve this, we propose a new runtime for the #zelus language, which simulates
|
|
assertions with their own solvers in order to maintain the separation between
|
|
assertions and the model they operate on.
|
|
|
|
#TODO()
|
|
|
|
#heading(outlined: false)[Arguments Supporting Their Validity]
|
|
What is the evidence that your solution is a good solution? (Experiments?
|
|
Proofs?) Comment on the robustness of your solution: does it rely on
|
|
assumptions, and if so, to what extent?
|
|
|
|
#TODO("Justify")
|
|
|
|
#heading(outlined: false)[Summary and Future Work]
|
|
What did you contribute to the area? What comes next? What is a good _next_ step
|
|
or question?
|
|
|
|
#TODO("Next steps")
|
|
|
|
#pagebreak()
|
|
#outline()
|
|
#pagebreak()
|
|
|
|
= Background
|
|
|
|
== Hybrid systems
|
|
|
|
Hybrid systems are dynamical systems whose behaviour evolves through both
|
|
continuous and discrete phases. They are used to model software interacting with
|
|
physical systems. Continuous phases are described using ordinary differential
|
|
equations (ODEs), while discrete phases can be represented as a reactive
|
|
program in a synchronous language such as #lustre or #esterel.
|
|
|
|
As a first example, say we wish to model a bouncing ball. We could start by
|
|
describing its distance from the ground $y$ with a second-order differential
|
|
equation
|
|
$ addot(y) = -9.81 $
|
|
where $addot(y)$ denotes the second order derivative of $y$ with
|
|
respect to time (the acceleration of the ball), and $9.81$ is the gravitational
|
|
constant $g$: the acceleration of the ball is its negation. We now give the
|
|
initial position and speed of the ball:
|
|
$ y(0) = 50 space space space adot(y)(0) = 0 $
|
|
We have just described an initial value problem: given an ODE and an initial
|
|
value for its dependent variable, its solution is a function $y(t)$ returning
|
|
the value of the variable at a given time $t$. We can find an approximation of
|
|
this function using an ODE solver, such as #sundials.
|
|
|
|
As of right now, our ball will fall until the end of time; we have not said
|
|
anything about how it bounces when it hits the floor. To do so, we need a notion
|
|
of discrete _events_. These are modelled by zero-crossings: we monitor a certain
|
|
value and stop when it goes from strictly negative to positive or null. For our
|
|
purposes, we choose $-y$ as the monitored value, and call the zero-crossing
|
|
event $z$. When $z$ occurs (i.e., when the ball touches the ground), we set the
|
|
speed $adot(y)$ to $-k dot "last"(adot(y))$, where $"last"(y)$ denotes the left
|
|
limit of $y$ (we cannot specify $adot(y)$ in terms of itself), and $k$ is a
|
|
factor modelling the loss of inertia due to the collision (say, $0.8$). We can
|
|
then resume the approximation of the solution.
|
|
|
|
@lst:ball.zls shows how such a model might be expressed in the concrete syntax
|
|
of #zelus.
|
|
|
|
#figure(placement: top, gap: 2em,
|
|
```zelus
|
|
let hybrid ball () = y where
|
|
rec der y = y' init 50.0
|
|
and der y' = -9.81 init 0.0 reset z -> -0.8 *. (last y')
|
|
and z = up (-. y)
|
|
```,
|
|
caption: [The bouncing ball in #zelus]
|
|
) <lst:ball.zls>
|
|
|
|
More formally, a hybrid system can be described as an automaton
|
|
|
|
== Executing models
|
|
|
|
Executing such a model is quite simple. There are two modes of execution:
|
|
discrete and continuous. In continuous mode, we call the ODE solver in order to
|
|
obtain an approximation of the variables defined through ODEs, and monitor for
|
|
zero-crossings. If a zero-crossing occurs, we enter the discrete mode, in which
|
|
we perform computation steps as needed, until no other zero-crossing occurs, in
|
|
which case we go back to the continuous mode, and repeat, as seen in @automaton.
|
|
|
|
#figure(finite.automaton(
|
|
(D: (D: "cascade", C: "no cascade"),
|
|
C: (C: "no zero-crossing", D: "zero-crossing")),
|
|
initial: "D", final: (), layout: finite.layout.linear.with(spacing: 3)
|
|
), caption: [High-level overview of the runtime], placement: top) <automaton>
|
|
|
|
= Runtime
|
|
To solve this issue, we need to redefine what the runtime of our hybrid system
|
|
models is. The runtime is the piece of software that handles the pairing of a
|
|
hybrid model with a solver and the different execution phases that need to take
|
|
place.
|
|
|
|
To allow for independent simulation of the assertions, we need to simulate them
|
|
with their own ODE solvers. Since assertions can themselves contain ODEs, they
|
|
can be viewed as hybrid systems themselves. Assertions can also contain their
|
|
own sub-assertions, and so recursively: our runtime needs to handle this
|
|
accordingly.
|
|
|
|
== Hybrid models with assertions
|
|
A hybrid model with assertions can be defined using a recursive data type:
|
|
```ocaml
|
|
type ('p, 'a, 'b, 'y, 'yder, 'zin, 'zout) hnode_a =
|
|
HNodeA : {
|
|
body : ('s, 'p, 'a, 'b, 'y, 'yder, 'zin, 'zout) hrec;
|
|
assertions : ('p, 's, unit, 'y, 'yder, 'zin, 'zout) hnode_a list;
|
|
} -> ('p, 'a, 'b, 'y, 'yder, 'zin, 'zout) hnode_a
|
|
```
|
|
|
|
Notice that the list of assertions takes as input the inner state of the parent
|
|
model: assertions are checked on the model state, and any variable which is
|
|
required by the assertion becomes a state variable.
|
|
|
|
== Solvers as synchronous nodes
|
|
== Simulations as synchronous nodes
|
|
#TODO("talk about the new runtime")
|
|
|
|
= Assertions
|
|
#TODO("talk about how assertions are done")
|
|
|
|
#pagebreak()
|
|
= Annex
|
|
#set heading(level: 2)
|
|
#bibliography("sources.bib", full: true)
|
|
#set heading(level: 1)
|