Worst Case Temporal Consistency in IntegratedModular Avionics Systems
Micha¨el Lauer, J´erˆome Ermont
Universit´e de Toulouse  IRIT  INPT/ENSEEIHT2, rue Camichel, BP 71231071 Toulouse Cedex 7, FranceEmail: ﬁrstname.name@enseeiht.frl
Fr´ed´eric Boniol, Claire Pagetti
ONERA2, avenue Edouard Belin BP 402531055 Toulouse Cedex, FranceEmail: ﬁrstname.name@onera.fr
Abstract
—Integrated Modular Avionics (IMA) architectureshave been deﬁned for sharing communication and computationresources. The aim of this paper is to evaluate temporal consistency properties of functions implemented on IMA platforms.More speciﬁcally, the two contributions are : (1) a modelingapproach for IMA platforms based on the
tagged signal model
and an abstraction of the network, (2) the deﬁnition of twoevaluation methods for temporal consistency properties. Theindustrial applicability of the method is demonstrated on anAirbus A380like platform. We also discuss the signiﬁcance of the overapproximations induced by the network abstraction.
Index Terms
—Realtime distributed systems, worstcase timinganalysis,
tagged signal model
, safety requirements
I. I
NTRODUCTION
A. Context: Integrated Modular Avionics architecture
The Integrated Modular Avionics (IMA) architecture hasbeen deﬁned in the avionics context for sharing communication and computation resources. Avionics functions executingon the platform must fulﬁll safety requirements, one of thembeing a strong segregation. For that purpose, airframers andthe ARINC corporation have proposed two standards. Thestandard ARINC 653 [1] speciﬁes the management of computing resources (named modules): the scheduling of functionson each module is deﬁned offline by a periodic sequenceof slots (named partitions) statically organized in a timedframe named the MAjor time Frame (MAF). Thus, eachfunction periodically executes at ﬁxed times. Modules howeverare globally asynchronous. The standard ARINC 664 [2],implemented in AFDX (Avionics FullDuplex Switched Ethernet) networks, describes the management of communicationresources (switches and endsystems). Communication ﬂowsare statically segregated into Virtual Links (VL). Each VL isdedicated to a single function and implements a trafﬁc shaper.It is characterized by a Bandwidth Allocation Gap (BAG), i.e.,the minimal time interval separating two successive messageson the VL. These two standards globally deﬁne the IMAconcept which has been implemented in the Airbus 380 and theBoeing 787 for instance. According to this deﬁnition, an IMAplatform can be seen as a set of modules, switches and linkscompliant to these standards. An
IMA system
is a platform onwhich a set of functions is statically mapped.Because of their critical nature, IMA systems must alsosatisfy strong realtime requirements such as latency requirements: an input must result in an output before a certainamount of time. In this paper, we focus on a less studiedrequirement: temporal consistency between data. Informally, if an input results in multiple outputs, then we need to guaranteethat the outputs are temporally consistent, i.e., all outputs mustoccur within a certain time window. Likewise, if an outputdepends on multiple inputs then the inputs must occur withina time window.
B. Case study: Flight Management System
To illustrate the approach, we consider the avionics casestudy in Figure 1, which is a part of a ﬂight managementsystem (FMS). This system manages part of the displays in thecockpit. It provides some information on a waypoint requestedby the pilot and periodically refreshes dynamic data related tothis waypoint (distance and estimated time of arrival).
Cockpit
KU
1
MFD
1
KU
2
MFD
2
XNDBXXFM2ADIRU2
RDC
2
sensor
2
XXADIRU1FM1
RDC
1
sensor
1
P artition period duration offset module
KU
1
(KU
2
)
50 25 0 1 (2)
MFD
1
(MFD
2
)
50 25 25 1 (2)
FM
1
(FM
2
)
60 30 0 3 (4)
ADIRU
1
(ADIRU
2
)
60 30 0 5 (6)
NDB
100 20 0 7
Fig. 1: Flight management system
System description.
In the cockpit, the pilot and the copilotuse a personal keyboard and two displays to interact with theFMS. Information displayed on both screens must be similaralthough they are not processed by the same components. TheFMS uses a redundant implementation of its functions whichare segregated on each side of the plane (named side 1 andside 2).
2011 IEEE 13th International Symposium on HighAssurance Systems Engineering
15302059/11 $26.00 © 2011 IEEEDOI 10.1109/HASE.2011.48212
At any time, the pilot can request some information on agiven waypoint. The
KU
1
(Keyboard and Cursor Control Unit)controls the physical device used by the pilot to enter hisrequests. When
KU
1
receives a request, it broadcasts it to theFlight Managers
FM
1
and
FM
2
. The
FM
s manage the ﬂightplan, i.e., the trajectory between successive waypoints. Whena request occurs, both query the
NDB
(Navigation Database)to retrieve the static information on the waypoint such as thelatitude and the longitude. The
NDB
separately answers each
FM
by sending a message containing the expected data. Uponreception of this message, each
FM
computes two complementary dynamic data: the distance to the waypoint, and theestimated time of arrival (ETA). These data are periodicallysent to the
FM
s respective
MFD
s (Multi Functional Display)which periodically elaborate the pages to be displayed on thescreens. To compute these data, the
FM
s use the position andthe speed of the aircraft which are periodically delivered bythe
ADIRU
s (Air Data Intertial Reference Unit). The
ADIRU
sdetermine the speed and position of the aircraft thanks to dataprovided by sensors. Here, we only consider the data providedby one sensor per
ADIRU
. The sensors communicate throughﬁeld networks. Interconnection with the AFDX network ismanaged by
RDC
s (Remote Data Concentrator).From this example we can see that a function can havetwo behaviors with respect to its data: periodic or sporadic.Sensors, RDCs, ADIRUs and MFDs write there output dataperiodically using the last input data received (thus a datacan be used several times before it is refreshed). For thesefunctions, input data are stored in
sampling ports
in which dataare continuously overwritten. On the contrary, the KUs and theNDB write there data sporadically in response to inputs. Thesefunctions use
queuing ports
to store their input data beforeconsuming them. The FMs use the two kinds of behaviors:periodic and sporadic.Each function is allocated in a partition of a module. Eachpartition is described by three realtime features: period of repetition, duration of the slot and offset in the MAF. The onlyassumption on a function implementation is that its executionis contained in its partition, i.e., we assume that its worst caseexecution time is equal to the duration of its partition and itsbest case execution time is zero. The allocation of the sides 1and 2 is symmetric. The realtime parameters are summarizedin Figure 1.
System requirements.
The functional architecture has to meetthe two following realtime requirements :
ϕ
1
: pages relative to a pilot request must be displayed within atime window of 450 ms. This involves the functional chains :
KU
1
FM
1
FM
2
NDBFM
1
FM
2
MFD
1
MFD
2
reqwpIdwpIdquery
1
query
2
answer
1
answer
2
wpInfo
1
wpInfo
2
disp
1
disp
2
ϕ
2
: the ETA must be calculated from redundant air pressurevalues measured within a time window of 300 ms. Thisinvolves the functional chains :
sens
1
RDC
1
ADIRU
1
FM
1
sens
2
RDC
2
ADIRU
2
pres
1
pres
1
ETA
1
pres
2
pres
2
speed
2
speed
1
C. Related work
Numerous works can be found in the literature on IMAsystems. A ﬁrst kind of work deals with the conﬁgurationgeneration of IMA systems. The authors of [3] propose anautomatic manner based on Integer Linear Programming (ILP)for allocating the functional speciﬁcations on the platformwhile ensuring some the safety (i.e., faulttolerance) requirements. In [4] also proposes a technique based on Mixed ILPto automatically allocate and schedule avionics functions onan IMA platform. The objective being the maximization of the spare resource on each module in order to meet futureresource demand growth.Other works focus on performance evaluation. The Network Calculus [5] and the
trajectory approach
[6] can be used todetermined upper bounds of network traversal time. The RealTime Calculus [7] (a variation of the Network Calculus) is anefﬁcient method to determine worst case latencies in realtimesystems. However these works deals with latency propertiesand do not consider more elaborate properties like temporalconsistency.The study of temporal consistency between data is relativelysparse in the literature. Temporal consistency is studied in realtime databases in [8] but the authors do not study the notionof functional chains. This notion can be found in [9], [10].
However, both papers do not deal with IMA assumptions and[9] evaluate temporal consistency through a simulation angleand thus cannot be used to provide safe guarantees to a criticalsystem.Upper bounds of endtoend properties in a networkedembedded system has been proposed in [11], where the authorsanalyze the properties by modeling the functional chainsand the network architecture as a set of timed automata. Inorder to cope with the combinatorial explosion, they proposeseveral abstractions. However, this work suffers from twoshortcomings with respect to our objective: (1) the architectureis not based on IMA hypothesis, and (2) the abstractionsremain insufﬁcient for realistic systems.We attempted in [12] to overcome these difﬁculties byextending [11] to IMA systems. We proposed a method basedon two consecutive steps: (1) abstraction of the network witha set of timed channels using the
trajectory approach
[6] ,and (2) veriﬁcation of the requirements with the U
PPAAL
model checker. This method allows to take into accountthe speciﬁcities of IMA systems. However, it suffers fromthe combinatorial explosion problem for functional chainscomposed of more than four functions.
D. Contribution and proposed approach
This paper focuses on worst case evaluation of temporalconsistency properties in IMA systems. As in [12], the approach is composed of two steps: (1) simpliﬁcation of thesystem by abstracting the network with a set of timed channels,
213
and (2) evaluation of the worst case temporal consistency onthe abstract system.
Abstraction of the network.
Combinatorial complexity of the worst case temporal consistency evaluation takes its rootin the asynchronism of the modules, the variability of theexecution times and indeterministic congestion in the network.We showed in [12] that taking into account all these factors inthe evaluation of high level properties is intractable. However,the complexity can be signiﬁcantly reduced by abstracting thenetwork with a set of timed channels. In this setting, each VLis abstracted with a channel characterized by a time interval
[
a,b
]
, where a (resp. b) is the lower (resp. upper) bound of thenetwork traversal time along the VL path. These bounds aredetermined with the
trajectory approach
[6] which has beensuccessfully applied to AFDX networks in [13].By way of example, in the FMS case study we considerthat each
VL
i
is abstracted by a timed channel
c
i
[0
.
12
,
2]
(in
ms
): each frame released by a
VL
i
trafﬁc shaper undergoesa delay between
0
.
12
ms
and
2
ms
to reach its destination.Note that this abstraction is an overapproximation becausethe bounds of the timed channels are determined with an overapproximative technique. We discuss the signiﬁcance of thispoint through experiments in section IV.
Temporal consistency evaluation.
This second step constitutes the main contribution. We use the
tagged signalmodel
[14] to describe all the possible behaviors of theabstract system and the temporal consistency requirements itmust satisfy (Section II). Evaluation of worst case temporalconsistency in this model allows us to verify the satisfactionof the requirements (Section III). Two methods are proposed:the ﬁrst one is a low complexity sufﬁcient test, whereas thesecond one is more involved (it requires solving Integer LinearPrograms) but allows for an exact evaluation. Experiments(Section IV) show that this higher complexity is manageableeven in large systems.II. S
EMANTIC OF ABSTRACT
IMA
SYSTEMS IN THETAGGED SIGNAL MODEL
This section describes how the behaviors of an IMA systemand the requirements it must satisfy can be expressed in the
tagged signal model
[14].
A. Intuition of the formalism
To give the intuition of our formalization in the
tagged signal model
, we detail the modeling of the function
MFD
1
.The idea is to describe all the possible behaviors of thefunction with the notions of
event
,
signal
and
process
.
MFD
1
produces the pages to be displayed (
disp
) on the pilotscreen and is periodically activated by module 1. This functionacquires its input at the activation, does some processing andproduces the page after at most
C
MFD
1
time unit. We now haveto describe how each event relates to each other.We note
t
MFD
1
n
the time of the
n
th event of activation of
MFD
1
and
t
dispn
the time of the event of production of the
n
thpage. Since we assume that the function produces its outputat most
C
MFD
1
after its activation, these times are related inthe following manner:
t
MFD
1
n
≤
t
dispn
≤
t
MFD
1
n
+
C
MFD
1
(1)In our model, we also track dependencies between events.For example, the
n
th
disp
depends on both the
n
th activationand the event of the last reception of waypoint information.To record the dependencies between events, we associate toeach event a value in addition to its timestamp (or tag). Wedeﬁne this value as a vector with as many components as thereare sources of events (activation of
MFD
1
, writing of
disp
,...)and each component represents the index of an event. We note
v
disp
n
the value associated to the
n
th
disp
. To distinguish thecomponents, we use a speciﬁc notation:
v
disp
n

wpInfo
=
k
, whichmeans that the
n
th event of
disp
depends on the
k
th event of
wpInfo
. Given the expected behavior of the function, we have,for all
n
∈
N
:
v
disp
n

MFD
1
=
n v
disp
n

disp
=
⊥
(2)We use the value
⊥
to signify the absence of dependency.Instances of
wpInfo
are received in a sampling port, whichmeans that they are continually overwritten and that
MFD
1
only reads the last received instance. We note
t
wpInfo
k
the arrivaltime of the
k
th instance of
wpInfo
in module 1. If the
k
thinstance of
wpInfo
is used to compute the
n
th page, then it isthe last
wpInfo
received before the
n
th activation of
MFD
1
,which can be expressed as:
v
disp
n

wpInfo
= max
l
{
t
wpInfo
l
≤
t
MFD
1
n
}
(3)Formally, an
event
is a tuple composed of a tag and a value
(
t,v
)
∈
R
×
(
N
∪⊥
)
N
for some
N
. In practice,
N
is the numberof sources of events considered in a system. A sequence of events relative to a source is called a
signal
. More precisely,a signal
s
belongs to the set
S
= 2
R
×
(
N
∪⊥
)
N
of all signals. Atuple,
(
s
MFD
1
,s
wpInfo
,s
disp
)
∈
S
3
, describes a possible behaviorof
MFD
1
iff all events of the signals
s
MFD
1
,
s
wpInfo
and
s
disp
satisfy the constraints (1), (2) and (3).A
process
is a set containing all possible behaviors of anelement. For example,
MFD
1
is deﬁned by the process
P
MFD
1
:
P
MFD
1
=
{
(
s
MFD
1
,s
wpInfo
,s
disp
)
∈
S
3

t
MFD
1
n
≤
t
dispn
≤
t
MFD
1
n
+
C
MFD
1
,v
disp
n

MFD
1
=
n, v
disp
n

disp
=
⊥
,v
disp
n

wpInfo
= max
l
{
t
wpInfo
l
≤
t
MFD
1
n
} }
B. Description of an abstract IMA system
Possible behaviors of interacting elements can be describedby the intersection of the element processes. However, thisintersection makes sense only if all the processes are set of tuples of the same
N
signals, where
N
is the number of sources of events considered in the model. Suppose that asystem is composed of a collection
P
of processes such that
∀
P
∈
P
,
P
⊆
S
N
. Then, all the possible behaviors of thesystem are deﬁned by:
S
=
P
∈
P
P
(4)
214
In the following we present the relevant signals and processes used in the description of an abstract IMA system.
1)
Relevant signals
:
To describe the behaviors of a systemwe use: (1) a signal per function in order to model its activations, (2) a signal for each sporadic triggering event (such asa request of the pilot), and (3) a signal for each local copy of data exchanged between the functions (such as the waypointidentiﬁer
wpId
) in order to model the updates. Since a datamay be sent across the platform, the local behavior depends onthe behavior of the hosting component. For example, the data
wpId
is emitted by
KU
1
(1 copy), crosses the trafﬁc shaper(1 copy) and takes 2 timed channels (2 copies) to reach
FM
1
and
FM
2
.We apply several naming conventions: the signal associatedto the activation of a function
f
will be denoted by
s
f
andthe signal of a copy of a data
z
at the output of an element
e
will be denoted by
s
z e
. For an event
s
j
[
i
]
we note
t
ji
its tagand
v
ji
its value. Let
s
j
[
i
] = (
t,
(
d
1
,...,d
N
))
be the
i
th eventof the signal
s
j
, if
d
k
=
⊥
, it means that
s
j
[
i
]
depends on the
d
k
th event of
s
k
. We also denote by
s
j
[
i
]

s
k
the value
d
k
. If the value of an event is
(
⊥
,...,
⊥
)
then it does not dependon any event. We use the symbol
⊥
to refer to
(
⊥
,...,
⊥
)
forshort. These notations are illustrated in the following example.
Example 1.
Let us consider a subset of the case study. Wesimply consider the elements from a request to the
FM
s: arequest of the pilot
req
is interpreted by
KU
1
as a waypoint identiﬁer wpId which is sent to
FM
1
and
FM
2
. Transmissionis done on
VL
1
which is multicast (frames are transmitted through two timed channels
c
1
and
c
′
1
). Upon reception of wpId each
FM
produces a
query
to retrieve information on thewaypoint. The ﬁgure below partially summarizes the system.
KU
1
VL
1
trafﬁc shaper req
c
1
[0
.
12
,
2]
c
′
1
[0
.
12
,
2]
FM
1
FM
2
Module 1 Module 2 Module 3
In this restricted example, there are exactly
N
= 10
signals:
s
req
,s
KU
1
,s
wpId KU
1
,s
wpId VL
1
,s
wpId c
1
,s
wpId c’
1
,s
FM
1
,s
query FM
1
,s
FM
2
,s
query FM
2
. By way of example,let us describe a possible behavior for the ﬁrst 3 signals
s
req
,s
KU
1
,s
wpId KU
1
:
KU
1
KU
1
KU
1
KU
1
s
req
: (30
,
⊥
) (135
,
⊥
)
s
KU
1
: (0
,
⊥
) (50
,
⊥
) (100
,
⊥
) (150
,
⊥
)
s
wp KU
1
: (65
,
(1
,
2
,
⊥
)) (160
,
(2
,
4
,
⊥
))
We suppose that module
1
starts at 0. KU
1
is the ﬁrst partition scheduled on module 1 and thus starts at
0
, then it is periodically activated every
50
ms
. The activations do not depend on any signal, thus
s
KU
1
=
{
(0
,
⊥
)
,
(50
,
⊥
)
,
(100
,
⊥
)
,...
}
.The ﬁrst request of the pilot is modeled by event
s
req
[1]
. It occurs at
30
ms
and is processed in the second executionKU
1
. We suppose that this processing takes
15
ms
∈
[0
,C
KU
1
]
,with
C
KU
1
the duration of the partition. At the end of this processing, KU
1
produces a copy of the data
wpId
at itsoutput. It is modeled by the event
s
wpId KU
1
[1]
. The value of thisevent with respect to
s
req
,s
KU
1
,s
wp KU
1
is
(1
,
2
,
⊥
)
, whichmeans that
s
wpId KU
1
[1]
depends on event
s
req
[1]
, event
s
KU
1
[2]
and does not depend on any event of
s
wpId KU
1
.2)
Relevant processes
:
There is a process for each element of the system (modules, functions, trafﬁc shapers, timedchannels, RDCs and sensors). All these processes express therelations as a set of constraints to be fulﬁlled by the signals.In the sequel, if a constraint is not speciﬁed on a value, thismeans that this value is equal to
⊥
.
For the modules
, the purpose is to describe all the admissible signals of activation of the functions hosted on a modulewith respect to the module starting time and the scheduling(deﬁned by the MAF). More precisely, the process of module
m
is deﬁned by:
P
m
=
{
s
∈
S
N
 ∃
φ
∈
[0
,
HP
[
,
∀
f
∈
m.
host
,
∀
n
∈
N
,t
f n
=
φ
m
+
o
f
+
n
·
T
f
}
where
m.
host
is the set of functions hosted by the module,
HP
=
lcm
f
∈
m.
host
(
p
f
)
is the hyperperiod of the functions and
φ
m
is the phase (or starting time) of the module. Modules areasynchronous and thus they may not start at the same time.The scheduling of a function
f
is deﬁned by its offset
o
f
which relates to the starting time of its module and its period
T
f
.
For the functions
, the purpose is to specify the relationsbetween the function and the consumed/produced data. Whendelivered to a function, a copy of a data is stored either into asampling or a queuing port. This implies different behaviors.The process of a function
f
(with only sampling ports) isdeﬁned by:
P
f
=
{
s
∈
S
N
∀
n
∈
N
,
∃
t
∈
[
t
f n
,t
f n
+
C
f
]
,
∀
v
k
f
∈
f.
out
,t
v
k
f n
=
tv
v
k
f n

x
=
n
if
x
=
f n
′
if
x
∈
f.
in
,x
→
v
k
f
∧
n
′
= max
l
{
t
xl
≤
t
f n
} }
where
C
f
is the duration of the partition,
f.
out
is the copiesof data produced by
f
,
f.
in
is the copies read by
f
stored ina sampling port, and
x
→
v
k
f
means that the value of
v
k
f
depends on the copy of data
x
. The tags specify that the dataare all produced at the same time
t
within the execution timeof
f
. The conditions on the values state that the
n
th copy isproduced at the
n
th execution of
f
, and that if
x
is an inputof
f
and is required to compute
v
k
f
then the computationuses the last copy stored in the module at the beginning of the
n
th execution, otherwise there is no dependency.We now specify the behavior of a function
f
having onlyqueuing ports. Its process is then deﬁned by:
P
f
=
{
s
∈
S
N
∀
u
∈
f.in,
∀
k
∈
N
,
∀
n
s.t.
t
uk
∈
]
t
f n
−
1
,t
f n
]
,
∃
t
∈
[
t
f n
,t
f n
+
C
f
]
,t
v f k
=
t, v
v f k

f
=
n,v
v f k

u
=
k,
with
v f
∈
f.out s.t. u
→
v f
}
215
At each execution,
f
processes all inputs arrived since the lastexecution. If there are
l
events of
s
u
during
]
t
f n
−
1
,t
f n
]
thenthere are
l
events of
s
v f
at
t
∈
[
t
f n
,t
f n
+
d
f
]
. Note that fora given execution, there may be no output event. An exampleof such a function is the NDB. It responds to queries receivedsince its last execution. If there is no new query it produces noanswer. Therefore, the production of its outputs is sporadic.On the contrary, a function with sampling ports like ADIRUproduces outputs for each execution even if no new data hasbeen received from the sensors. Such a function always usesthe last input. The ADIRU produces its outputs periodicallyand independently of its inputs refresh.These behaviors can be mixed in order to describe morecomplex functions such as the
FM
s which use both samplingand queuing ports.
For the trafﬁc shaper
, the purpose is to express theregulation of the packets on the VL to ensure the BAG. Thisregulation speciﬁes the relation on the signals of the copy of the data emitted by the VL. The process of the trafﬁc shaperof
VL
is deﬁned by:
P
VL
=
{
s
∈
S
N
∀
n
∈
N
,f.
out
→
VL
=
{
v
i
1
f,...,v
i
l
f
}
t
v
ij
VL
n
=
t
v
ij
f n
+
c
nj
·
bag
,
j
c
nj
=
{
0
,...,l
−
1
}
v
v
ij
VL
n

v
ij
f
=
n
}
where the set
f.
out
→
VL
=
{
v
i
1
f,...,v
i
l
f
}
gives the dataproduced by
f
and emitted on
VL
. There is a timing delayof
bag
between two successive emissions. All transmissionsorders are possible between the copies of
v
i
j
VL
. The valuesstates that the
n
th copy of
v
i
j
VL
depends on the
n
th copy of
v
i
j
f
. The trafﬁc shaper is assumed to be correctly designed,i.e., it does not lose frames and all frames are transmittedbefore the next period of
f
.
For the timed channels
, the purpose is to describe thetemporal behavior of the copies of the data along a path. Theprocess associated to the timed channel
c
connected to
VL
isdeﬁned by:
P
c
=
{
s
∈
S
N
∀
n
∈
N
,
∀
v
VL
,t
v cn
∈
[
t
v
VL
n
+
a
c
,t
v
VL
n
+
b
c
]
,v
v cn

v
VL
=
n
}
The timed channel emits the packet within the interval
[
a
c
,b
c
]
,thus all data emitted by the trafﬁc shaper
VL
are duplicated inthe timed channel and their tags are delayed by a value withinthe interval.
For the sensors
, the purpose is to describe all the admissiblesequences of production of data. A sensor has an initial phaseand a sampling period. The process of a sensor
sens
is deﬁnedby:
P
sens
=
{
s
∈
S
N
 ∃
φ
∈
[0
,T
[
,
∀
n
∈
N
,t
v sensn
=
φ
+
n
·
T
}
where
v
is the data produced by
sens
,
T
is its period and
φ
its initial phase.
For the
RDC
s
, the purpose is to describe a bridge betweenthe sensors and the AFDX network. The RDC periodicallyencapsulates the last data received into frames and deliversthem to VL trafﬁc shapers. Thus its behavior can be seen asthe composition of a module hosting only one partition. Theprocess associated to the
RDC
r
is:
P
r
=
{
s
∈
S
N
∃
φ
∈
[0
,T
[
,
∀
n
∈
N
,
∃
t
∈
[
n
·
T,n
·
T
+
C
]
,
∀
v
s
r
∈
r.out,t
v
s
rn
=
φ
+
t,v
v
s
rn

x
=
k
if
x
=
rn
′
if
x
∈
r.
in
,x
→
v
s
r
∧
n
′
= max
l
{
t
xl
≤
φ
+
n
·
T
}}
where
C
is the worst case execution time of
r
,
r.
out
is thecopies of data produced by
r
,
r.
in
is the copies of dataconsumed by
r
and
x
→
v
k
r
means that the value of
v
k
r
depends on the data
x
.
C. Requirement semantic
In this paper we focus on temporal consistency of divergent/convergent functional chains. We believe that this tworequirements are the most relevant to the industry. For thesake of clarity, the deﬁnitions are given for only two functionalchains. Generalization to
n
chains is straightforward.
1) Temporal consistency of divergent functional chains:
A temporal consistency requirement between divergent functional chains is expressed on chains sharing at least a data (andthe function processing the data) at their beginning. Let
C
=
v
0
→
F
1
v
1
→
...
F
nv
n
→
and
C
′
=
v
′
0
→
F
′
1
v
′
1
→
...
F
′
n
′
v
′
n
′
→
be two functionalchains such that
v
0
=
v
′
0
and
F
1
=
F
′
1
.The requirement
Consist
Λ
(
C
,
C
′
)
is satisﬁed for the upperbound
Λ
iff for all possible behaviors of the system, each eventon
v
0
results in events on
v
n
and
v
′
n
′
occurring at a distanceless than
Λ
. This is formalized in the TSM by:
S

=
Consist
≤
Λ
(
C
,
C
′
)
⇐⇒ ∀
s
∈
S
,
∀
(
i,j,k
)
∈
N
3
, s.t. s
v
0
[
k
]
→
s
v
n
[
i
]
and
s
v
0
[
k
]
→
s
v
′
n
′
[
j
]

t
v
n
F
n
i
−
t
v
′
n
′
F
′
n
′
j
 ≤
Λ
(5)
where
s
v
0
[
k
]
→
s
v
n
[
i
]
means that event
s
v
n
[
i
]
dependsby transitivity on event
s
v
0
[
k
]
: there exists a chain of eventspropagating dependencies between this two events.
2) Temporal consistency of convergent functional chains:
A temporal consistency requirement between convergent functional chains is expressed on chains sharing at least a data (andthe function processing the data) at their end. Let
C
=
v
0
→
F
1
v
1
→
...
F
nv
n
→
and
C
′
=
v
′
0
→
F
′
1
v
′
1
→
...
F
′
n
′
v
′
n
′
→
be two functional chainssuch that
v
n
=
v
′
n
′
and
F
n
=
F
′
n
′
.The requirement
Consist
Λ
(
C
,
C
′
)
is satisﬁed for the upperbound
Λ
iff for all possible behaviors of the system, each eventon
v
n
depends on events
v
0
and
v
′
0
happening at a distanceless than
Λ
. This is formalized in the TSM by:
S

=
Consist
≤
Λ
(
C
,
C
′
)
⇐⇒ ∀
s
∈
S
,
∀
(
i,j,k
)
∈
N
3
, s.t. s
v
0
[
i
]
→
s
v
n
[
k
]
and
s
v
′
0
[
j
]
→
s
v
n
[
k
]

t
v
0
i
−
t
v
′
0
j
 ≤
Λ
(6)
216