243 lines
11 KiB
Typst
243 lines
11 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 note(color, prefix, ..what) = {
|
|
let msg = if what.pos().len() == 0 { "" } else { ": " + what.pos().join("") }
|
|
block(fill: color, width: 100%, inset: 5pt, align(center, raw(prefix + msg)))
|
|
}
|
|
#let TODO(..what) = note(red, "TODO", ..what)
|
|
#let MENTION(..what) = note(gray, "MENTION", ..what)
|
|
#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 an illustration, say we wished to model an extensively studied system: a
|
|
bouncing ball. We could start by describing its distance from the ground $y$ as
|
|
a function of time, with a second-order differential equation
|
|
$ addot(y) = -9.81, $
|
|
where $addot(y)$ denotes the second order derivative of $y$ with
|
|
respect to time $(d^2y)/(d t^2)$ (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 _events_: we need to identify exactly when the ball hits the ground, so that
|
|
we may take action to make it bounce. These events 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 #raw(lang: "zelus", "last")\(adot(y))$, where
|
|
$#raw(lang: "zelus", "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 @cit:zelus_sync_lng_with_ode.
|
|
|
|
#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, and as done in @cit:alg_ana_hyb_sys, a hybrid system $cal(H)$ can
|
|
be defined as a graph whose nodes represent continuous behaviour, and whose
|
|
edges represent discrete transitions:
|
|
$ cal(H) = (L o c, V a r, E d g, A c t, I n v, I n i) $
|
|
where:
|
|
- $L o c$ is a finite set of _locations_;
|
|
- $V a r$ is a finite set of _variables_;
|
|
- $E d g subset.eq L o c times F times L o c$ is a finite set of _transitions_
|
|
|
|
|
|
== Executing models
|
|
|
|
To execute such a model, we first compile it into a synchronous function, as
|
|
described in @cit:sync_based_codegen_hyb_sys_lng. The details of this
|
|
compilation step are not particularly relevant to our purposes, and can be
|
|
ignored. What is more interesting is the output of this compilation step: a
|
|
single synchronous function. The simulation loop is then itself described as a
|
|
synchronous function operating on
|
|
|
|
#MENTION("Use of a single solver")
|
|
|
|
#pagebreak()
|
|
|
|
// The compilation of a hybrid model into a synchronous function is described in
|
|
// detail in @cit:sync_based_codegen_hyb_sys_lng, but can be summarized quite
|
|
// succintly as follows. By pairing this synchronous function with an
|
|
// off-the-shelf ODE solver like #sundials, we can then simulate the dynamics of
|
|
// the system. This is done by repeatedly performing execution steps according to
|
|
// two different modes: discrete and continuous.
|
|
|
|
// The continuous mode operates as follows: we first call the ODE solver in order
|
|
// to approximate the dynamics of the model's continuous state.
|
|
|
|
// Continuous steps first call the ODE solver to approximate the dynamics of the
|
|
// model's continuous variables. The solver will return a function defined on a
|
|
// time interval, which we then provide as input to the zero-crossing solver, which
|
|
// will monitor the evolution of zero-crossing values along this interval. After
|
|
// both solvers have been called, we choose what the next step's mode will be:
|
|
// - if no zero-crossings have been detected, we output the entire solution
|
|
// provided by the ODE solver, and the next step remains continuous;
|
|
// - if a zero-crossing occurs, we return the solution provided by the ODE solver
|
|
// up to the zero-crossing instant, and the next step becomes a discrete step.
|
|
|
|
// Discrete steps perform state changes and side effects. We first call the model's
|
|
// step function, which updates the state and outputs a value. We then decide what
|
|
// the next step is. If a zero-crossing event occured due to the current step, the
|
|
// next step is another discrete step. If no new event occured, we perform a
|
|
// continuous step.
|
|
|
|
// 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
|
|
#MENTION("the new runtime")
|
|
|
|
= Assertions
|
|
#MENTION("how assertions are done")
|
|
|
|
#pagebreak()
|
|
= Annex
|
|
#set heading(level: 2)
|
|
#bibliography("sources.bib", full: true)
|
|
#set heading(level: 1)
|