Theory Introduction
chapter‹A Gentle Introduction to TESL›
theory Introduction
imports Main
begin
section ‹Context›
text‹
The design of complex systems involves different formalisms for modeling their different parts or
aspects. The global model of a system may therefore consist of a coordination of concurrent
sub-models that use different paradigms such as differential equations, state machines,
synchronous data-flow networks,
discrete event models and so on, as illustrated in \autoref{fig:het-timed-system}.
This raises the interest in architectural composition languages
that allow for ``bolting the respective sub-models together'', along their various interfaces, and
specifying the various ways of collaboration and coordination~\<^cite>‹"nguyenvan:hal-01583815"›.
We are interested in languages that allow for specifying the timed coordination of subsystems by
addressing the following conceptual issues:
▪ events may occur in different sub-systems at unrelated times, leading to ∗‹polychronous› systems,
which do not necessarily have a common base clock,
▪ the behavior of the sub-systems is observed only at a series of discrete instants, and time
coordination has to take this ∗‹discretization› into account,
▪ the instants at which a system is observed may be arbitrary and should not change its behavior
(∗‹stuttering invariance›),
▪ coordination between subsystems involves causality, so the occurrence of an event may enforce
the occurrence of other events, possibly after a certain duration has elapsed or an event has
occurred a given number of times,
▪ the domain of time (discrete, rational, continuous. . . ) may be different in the subsystems,
leading to ∗‹polytimed› systems,
▪ the time frames of different sub-systems may be related (for instance, time in a GPS satellite
and in a GPS receiver on Earth are related although they are not the same).
›
text‹
\begin{figure}[htbp]
\centering
\includegraphics{glue.pdf}
\caption{A Heterogeneous Timed System Model}
\label{fig:het-timed-system}
\end{figure}›
consts dummyInfty :: ‹'a ⇒ 'a›
consts dummyTESLSTAR :: ‹'a›
consts dummyFUN :: ‹'a set ⇒ 'b set ⇒ 'c set›
consts dummyCLOCK :: ‹'a set›
consts dummyBOOL :: ‹bool set›
consts dummyTIMES :: ‹'a set›
consts dummyLEQ :: ‹'a ⇒ 'a ⇒ bool›
notation dummyInfty (‹(_⇧∞)› [1000] 999)
notation dummyTESLSTAR (‹TESL⇧*›)
notation dummyFUN (infixl ‹→› 100)
notation dummyCLOCK (‹𝒦›)
notation dummyBOOL (‹𝔹›)
notation dummyTIMES (‹𝒯›)
notation dummyLEQ (infixl ‹≤⇩𝒯› 100)
text‹
In order to tackle the heterogeneous nature of the subsystems, we abstract their behavior as clocks.
Each clock models an event, i.e., something that can occur or not at a given time. This time is measured
in a time frame associated with each clock, and the nature of time (integer, rational, real, or any
type with a linear order) is specific to each clock.
When the event associated with a clock occurs, the clock ticks. In order to support any kind of
behavior for the subsystems, we are only interested in specifying what we can observe at a series
of discrete instants. There are two constraints on observations: a clock may tick only at an
observation instant, and the time on any clock cannot decrease from an instant to the next one.
However, it is always possible to add arbitrary observation instants, which allows for stuttering
and modular composition of systems.
As a consequence, the key concept of our setting is the notion of a clock-indexed Kripke model:
@{term ‹Σ⇧∞ = ℕ → 𝒦 → (𝔹 × 𝒯)›}, where @{term ‹𝒦›} is an enumerable set of clocks, @{term ‹𝔹›}
is the set of booleans -- used to indicate that a clock ticks at a given instant -- and @{term ‹𝒯›}
is a universal metric time space for which we only assume that it is large enough to contain all
individual time spaces of clocks and that it is ordered by some linear ordering @{term ‹(≤⇩𝒯)›}.
›
text‹
The elements of @{term ‹Σ⇧∞›} are called runs. A specification language is a set of
operators that constrains the set of possible monotonic runs. Specifications are composed by
intersecting the denoted run sets of constraint operators.
Consequently, such specification languages do not limit the number of clocks used to model a
system (as long as it is finite) and it is always possible to add clocks to a specification.
Moreover, they are ∗‹compositional› by construction since the composition of specifications
consists of the conjunction of their constraints.
›
text‹
This work provides the following contributions:
▪ defining the non-trivial language @{term ‹TESL⇧*›} in terms of clock-indexed Kripke models,
▪ proving that this denotational semantics is stuttering invariant,
▪ defining an adapted form of symbolic primitives and presenting the set of operational
semantic rules,
▪ presenting formal proofs for soundness, completeness, and progress of the latter.
›
section‹The TESL Language›
text‹
The TESL language \<^cite>‹"BouJacHarPro2014MEMOCODE"› was initially designed to coordinate the
execution of heterogeneous components during the simulation of a system. We define here a minimal
kernel of operators that will form the basis of a family of specification languages, including the
original TESL language, which is described at \url{http://wdi.supelec.fr/software/TESL/}.
›
subsection‹Instantaneous Causal Operators›
text‹
TESL has operators to deal with instantaneous causality, i.e., to react to an event occurrence
in the very same observation instant.
▪ ▩‹c1 implies c2› means that at any instant where ▩‹c1› ticks, ▩‹c2› has to tick too.
▪ ▩‹c1 implies not c2› means that at any instant where ▩‹c1› ticks, ▩‹c2› cannot tick.
▪ ▩‹c1 kills c2› means that at any instant where ▩‹c1› ticks, and at any future instant,
▩‹c2› cannot tick.
›
subsection‹Temporal Operators›
text‹
TESL also has chronometric temporal operators that deal with dates and chronometric delays.
▪ ▩‹c sporadic t› means that clock ▩‹c› must have a tick at time ▩‹t› on its own time scale.
▪ ▩‹c1 sporadic t on c2› means that clock ▩‹c1› must have a tick at an instant where the time
on ▩‹c2› is ▩‹t›.
▪ ▩‹c1 time delayed by d on m implies c2› means that every time clock ▩‹c1› ticks, ▩‹c2› must have
a tick at the first instant where the time on ▩‹m› is ▩‹d› later than it was when ▩‹c1› had ticked.
This means that every tick on ▩‹c1› is followed by a tick on ▩‹c2› after a delay ▩‹d› measured
on the time scale of clock ▩‹m›.
▪ ▩‹time relation (c1, c2) in R› means that at every instant, the current time on clocks ▩‹c1›
and ▩‹c2› must be in relation ▩‹R›. By default, the time lines of different clocks are
independent. This operator allows us to link two time lines, for instance to model the fact
that time in a GPS satellite and time in a GPS receiver on Earth are not the same but are
related. Time being polymorphic in TESL, this can also be used to model the fact that the
angular position on the camshaft of an engine moves twice as fast as the angular position
on the crankshaft~⁋‹See \url{http://wdi.supelec.fr/software/TESL/GalleryEngine} for more details›.
We may consider only linear arithmetic relations to restrict the problem to a domain where
the resolution is decidable.›
subsection‹Asynchronous Operators›
text‹
The last category of TESL operators allows the specification of asynchronous relations between
event occurrences. They do not specify the precise instants at which ticks have to occur,
they only put bounds on the set of instants at which they should occur.
▪ ▩‹c1 weakly precedes c2› means that for each tick on ▩‹c2›, there must be at least one tick
on ▩‹c1› at a previous or at the same instant. This can also be expressed by stating
that at each instant, the number of ticks since the beginning of the run must be lower or
equal on ▩‹c2› than on ▩‹c1›.
▪ ▩‹c1 strictly precedes c2› means that for each tick on ▩‹c2›, there must be at least one tick
on ▩‹c1› at a previous instant. This can also be expressed by saying that at each instant,
the number of ticks on ▩‹c2› from the beginning of the run to this instant, must be lower or
equal to the number of ticks on ▩‹c1› from the beginning of the run to the previous instant.
›
no_notation dummyInfty (‹(_⇧∞)› )
no_notation dummyTESLSTAR (‹TESL⇧*›)
no_notation dummyFUN (infixl ‹→› 100)
no_notation dummyCLOCK (‹𝒦›)
no_notation dummyBOOL (‹𝔹›)
no_notation dummyTIMES (‹𝒯›)
no_notation dummyLEQ (infixl ‹≤⇩𝒯› 100)
end