=Paper=
{{Paper
|id=Vol-1085/16-paper
|storemode=property
|title=Towards a formal language for systemic requirements
|pdfUrl=https://ceur-ws.org/Vol-1085/16-paper.pdf
|volume=Vol-1085
|dblpUrl=https://dblp.org/rec/conf/csdm/Hourdel13
}}
==Towards a formal language for systemic requirements==
https://ceur-ws.org/Vol-1085/16-paper.pdf
Towards a formal language for systemic
requirements
Yann Hourdel
LIX, École Polytechnique, 91128 Palaiseau Cedex, France,
yann.hourdel@polytechnique.edu
Abstract. This work is an attempt to contribute to the field of systems
architecture. More precisely, it deals with complex1 engineered systems
analysis. Many informal methods for architecting such systems have been
described over the past decade, but a lot of specific points still need
to be clarified by a precise (mathematically formalized) definition. In
particular, the languages used to manipulate system properties during
systemic analysis are one big issue to be tackled. Our approach is the
following: we take the framework described in [6] and reviewed in [4]
as a starting point, and build a formal language to express functional
(behaviour) requirements on models. The result is a formal language
that allows architects to manipulate precise constraints on their models
and, more importantly, translate them across subsequent systemic levels.
Keywords: Systems modeling, Systems architecture, Systems Engineer-
ing, Architecture framework
Introduction
In this work, systems are seen as black boxes. Their behaviour is only functional,
so we will only express functional constraints on them. This kind of constraints is
one perfect thing to be formalized, since it is very close to mathematical notions.
Moreover, let us precise some important points:
– This work only deals with deterministic systems, for which we are able to
describe the set of possible executions.
– In this work, time is considered discrete. That allows us to speak about the
previous or next instant of an t.
1
large, integrated, dense and heterogeneous
Proceedings of the Posters Workshop at CSD&M 2013 175
Towards a formal language for systemic requirements
Notations
In the present work, the concatenation of two vectors A and B will be noted
A ⊗ B.
More generally, we will note f ⊗ g : A ⊗ C → B ⊗ D the concatenation of
f : A → B and g : C → D.
1 Preliminary definitions
In this section, we recall the definitions introduced in [3] and reviewed in [4] to
formalize the notion of system, a timed extension of Mealy machines to model
heterogeneous integrated systems and their integration.
Definition 1 (Type). The notion of type will be the classical “set of values”
one.
1.1 Time
Time is an underlying, yet very important, point of our formal approach. Indeed,
real-life systems are naturally described according to various types of “times”.
As a result, we need to deal uniformaly with both continuous and discrete times.
While this problem has been shown hard by [2], some solutions have been found
in studies like [5] to introduce formal models for mixed discrete-continuous sys-
tems. We give here a set of definitions to handle such systems.
Informally, as very well expressed in [3], time is “a linear quantity composed
of ordered moments, pairs of which define durations”.
Definition 2 (Time reference). A time reference is an infinite set T to-
gether with an internal law +T : T × T → T and a pointed subset (T + , 0T )
satisfying the following conditions:
– upon T + :
• ∀a, b ∈ T + , a +T b ∈ T + closure (∆1 )
• ∀a, b ∈ T + , a +T b = 0T =⇒ a = 0T ∧ b = 0T initiality (∆2 )
• ∀a ∈ T + , 0T +T a = a neutral to left (∆3 )
– upon T :
• ∀a, b, c ∈ T, a +T (b +T c) = (a +T b) +T c associativity (∆4 )
• ∀a ∈ T, a +T 0T = a neutral to right (∆5 )
• ∀a, b, c ∈ T, a +T b = a +T c =⇒ b = c cancelable to left (∆6 )
• ∀a, b ∈ T, ∃c ∈ T + , (a +T c = b) ∨ (b +T c = a) linearity (∆7 )
Definition 3 (Time scale). A time scale is any subset T of a time reference
T such that:
– T has a minimum mT ∈ T
– ∀t ∈ T, Tt+ = {t0 ∈ T | t ≺ t0 } has a minimum called succT (t)
Proceedings of the Posters Workshop at CSD&M 2013 176
Towards a formal language for systemic requirements
– ∀t ∈ T , when mT ≺ t, the set Tt− = {t0 ∈ T | t0 ≺ t} has a maximum called
predT (t)
– the principle of induction2 is true on T.
The set of all time scales on T is noted T s(T ).
1.2 Dataflows
Together with this unified definition of time, we need a definition of data that
allows to handle the heterogeneity of data among real-life systems. We rely on
the previous definitions to describe data carried by dataflows.
Definition 4 (-alphabet). A set D is an -alphabet if ∈ D. For any set
B, we can define an -alphabet by B = B ∪ {}.
Definition 5 (System dataset). A system dataset, or dataset, is a pair
D = (D, B) such that:
– D is an -alphabet
– B, called data behavior, is a pair (r, w) with r : D → D and w : D×D → D
such that3 :
• r() = (R1)
• r r(d) =r(d) (R2)
• r w(d, d0 ) = r(d0 ) (R3)
• w r(d0 ), d = d (W1)
• w w(d, d0 ), r(d0 ) = w(d, d0 ) (W2)
Definition 6 (Dataflow). Let T be a time scale. A dataflow over (D, T) is a
mapping X : T → D.
Definition 7 (Sets of dataflows). The set of all dataflows over (D, T) is
noted DT . The set of all dataflows
[ over D with any possible time scale on time
reference T is noted DT = DT .
T∈T s(T )
1.3 Systems and integration operators
Given the previous definitions, we are now able to give a mathematical definition
of systems. Informally, our definition is very similar to timed Mealy machines
with two important differences: the set of states may be infinite and the transfer
function transforms dataflows. The key point is to see those systems as black
boxes that just behave the way they are supposed to.
Definition 8 (System). A system is a 7-tuple ∫ = (T, X, Y, Q, q0 , F, δ) where:
2
For A ⊂ T, mT ∈ A & ∀t ∈ A, succT (t) ∈ A ⇒ A = T.
3
These axioms give a relevant semantics and are necessary to define consistent pro-
jections of dataflows on time scales.
Proceedings of the Posters Workshop at CSD&M 2013 177
Towards a formal language for systemic requirements
– T is a time scale,
– X, Y are input and output datasets,
– Q is a nonempty -alphabet 4 of states,
– q0 is an element of Q, called initial state,
– F : X × Q × T → Y describes a functional behavior,
– δ : X × Q × T → Q describes a state behavior.
Figure 1 illustrates this definition.
X(t) Q(t) Y(t)
Fig. 1. Illustration of a system
Example 1. A very basic radiator with an internal thermostat placed in a room
can be modeled as a system S = (T, X, Y, Q, q0 , F, δ) with:
– T ∼N
– X = room temperature ∼ R
– Y = {heat, nothing}
– Q = {qon , qof f }
– q0 = qof f (
heat if q(t) = qon
– F(x(t), q(t)) =
∅ otherwise
– δ is a follows:
x(t) < θ⊥
qof f qon
x(t) > θ>
It is important to understand here that at each time instant of the time scale,
the state of the system changes instantly and before F computes the resulting
output. At mTs , the beginning of the time scale, the state of the system is q0 .
But as soon as the first input data arrives, at succT (mTs ), the state of ∫ changes
so that the functional behaviour ignores q0 . Figure 2 illustrates this behaviour
and we give the following formal definition for timed executions of systems.
4
Defining Q as an -alphabet (therefore containing ) and not just as a set will make
it possible to define a dataflow of states, which is convenient.
Proceedings of the Posters Workshop at CSD&M 2013 178
Towards a formal language for systemic requirements
x1 x2 ...
Input/Output
q0 q1 q2 ... Time
Transition
dependencies
y1 y2 ...
Fig. 2. Transitions of a system throughout its time scale
Definition 9 (Execution of a system). Let ∫ = (T, X, Y, Q, q0 , F, δ) be a
˜ = InT . The execution
system. Let In ∈ X T be an input dataflow for ∫ and In
of ∫ on the input dataflow In is the 3-tuple (In, S, Out) where:
– S ∈ QT is recursively defined by:
• S(mT ) = δ In(m
˜ T
), q0 , mT
• ∀t ∈ T, S(t+ ) = δ In(t˜ + ), S(t), t+
where t+ = succT (t)
– Out ∈ Y T is defined by:
• Out(mT ) = F In(m˜ T
), q0 , mT
• ∀t ∈ T, Out(t+ ) = F In(t ˜ + ), S(t), t+
where t+ = succT (t)
In, S and Out are respectively input, state and output dataflows.
We note exec(∫ ) the set of possible executions of ∫ .
Definition 10 (Product of systems on a time scale). Let (∫ i )i = (T, Xi , Yi , Qi , q0 i, Fi , δi )i
be n systems of time scale T. The product ∫ 1 ⊗· · ·⊗∫ n is the system T, X, Y, Q, q0 , F, δ
where:
– X = X1 ⊗ · · · ⊗ Xn and Y = Y1 ⊗ · · · ⊗ Yn
– Q = Q1 × · · · × Qn and q0 = (q0 1 , . . . , q0 n ) = q0 1...n
– F x1...n , q1...n , t = F1 (x1 , q1 , t), . . . , Fn (x1 , q1 , t)
– δ x1...n , q1...n , t = δ1 (x1 , q1 , t), . . . , δn (x1 , q1 , t)
Remark 1. This definition can be extended to systems that do not share a time
scale, thanks to a technical operator introduced in [3]. This operator builds a
timed-extension of a system, which is a system that has an equivalent input-
output behaviour as the original system, but on a wider time scale. Figure 3
illustrates this idea.
Definition 11 (Feedback of a system). Let ∫ = T, (D×In, I), (D×Out, O), Q, q0 , F, δ
be a system such that there is no instantaneous influence of dataset D from
Proceedings of the Posters Workshop at CSD&M 2013 179
Towards a formal language for systemic requirements
T
Time shift inside
Ts
X''(t) Q''(t) Y''(t)
Fig. 3. Product of systems
the input to the output5 , i.e. ∀t ∈ T, ∀x ∈ In, ∀d ∈ D, F (d, x), q, t D =
F (, x), q, t D . The feedback of D in ∫ is the system ∫F B(D) = T, (In, I 0 ), (Out, O0 ), Q, q0 , F 0 , δ 0
where:
– I 0 is the restriction of I to In, and O0 is the restriction of O to Out
– F 0 (x ∈ In, q ∈ Q, t) = F (dx,q,t , x), q, t Out
– δ 0 (x ∈ In, q ∈ Q, t) = δ (dx,q,t , x), q, t
where dx,q,t stands for F (, x), q, t D .
Figure 4
Definition 12 (Abstraction of a transfer function). Let F : X T → Y T be
a transfer function. Let Ax : X T → Ya Ta be an abstraction for input dataflows
and Ay : Y T → Ya Ta an abstraction for output dataflows. The abstraction of
F for input and output abstractions (Ax , Ay ) with events E is the new transfer
function
Fa : (Xa ⊗ E)T → Ya Ta
defined by:
∀x ∈ X T , ∃e ∈ E Ta , Fa Ax (xT ) ⊗ e = Ay F (x)
Figure 5 illustrates this definition.
5
As explained informally in [3], this condition makes it possible to define a unique
feedback, i.e. without having to solve a fixed point equation that could lead to zero
or multiple solutions
Proceedings of the Posters Workshop at CSD&M 2013 180
Towards a formal language for systemic requirements
T
Ts
X(t) Y(t)
Fig. 4. Feedback of a system
-1
A Ao
i
X'(t) Y'(t)
Abstract transfer function Fa
Fig. 5. Abstraction of a transfer function
Definition 13 (Abstraction of a system). Let ∫ = T, X, Y, Q, q0 , F, δ be
a system. ∫ 0 = Ta , Xa ⊗ E, Ya , Qa , qa0 , Fa , δa is an abstraction of ∫ for input
and output abstractions (Ax , Ay ) if, and only if: ∃Aq : QT → Qa Ta , for all
execution (x, q, y) of ∫ , ∃E ∈ E Ta , Ax (xT ) ⊗ E, Aq (q), Ay (y) is an execution of
∫ 0 . Conversely, ∫ 0 is a concretization of the system ∫ .
A system captures the behavior of a system that can be observed (functional
and states behavior, called together systemic behavior ). From this definition, we
can start expressing behaviour properties.
2 Systemic behaviour properties: a formal semantics
The goal of this section is to be able to describe the behaviour of such a system,
in order to express properties and constraints on it. To do so, we will define a
Proceedings of the Posters Workshop at CSD&M 2013 181
Towards a formal language for systemic requirements
semantics of systems and provide a formal definition of “properties”. The idea
here is that systems are described by executions, so we must use timed properties.
We will first describe our property syntax language, then our property semantics.
Definition 14 (System property formulas). Let ∫ = (T, X, Y, Q, q0 , F, δ) be
a system.
The set P (∫ ) of property formulas over ∫ , similar to LTL6 , is inductively defined
as follows.
Here are the atomic formulas, where (x, q, y) ∈ X × Q × Y :
– input(x), which means that the current input of ∫ has to be x
– istate(q), which means that the current state of ∫ has to be q
– ouput(y), which means that the current output of ∫ has to be y
And here are the operators, where (φ, φ1 , φ2 ) ∈ P (∫ )3 :
– ¬φ
– φ1 ∧ φ2
– φ, which means that φ has to hold at the next state of the execution
– φ1 Uφ2 , which means that φ2 eventually has to hold and until it does, φ1 has
to hold (φ1 can hold further)
Definition 15 (Other system property formulas). Let ∫ = (T, X, Y, Q, q0 , F, δ)
be a system.
Let (φ, φ1 , φ2 ) ∈ P (∫ )3 .
The previously defined language P (∫ ) can be extended with the following opera-
tors:
– >
– ⊥
– φ1 ∨ φ2
– φ1 ⇒ φ2 7
– ♦φ, which means that φ has to hold now or in a future state of the execution
– φ, which means that φ has to hold for the entire subsequent execution
– φ1 Rφ2 , which means that φ1 has to hold until and including a state when φ2
holds, which is not forced to happen if φ1 holds forever
P (∫ ) is the syntax of our properties language. It gives us a way to express
properties on executions of ∫ . We are now able to define our semantics. The
following rules describe the satisfaction of P (∫ ) formulas using only the first
set of operators, but such rules could be easily extended to the extended set of
operators.
Definition 16 (system property satisfaction). Let ∫ be a system.
The satisfaction of a P (∫ ) formula φ by an execution e of ∫ , written e φ, is
defined according to the following rules:
6
see [1]
7
We can also accept φ1 ⊗ φ2 or any other “usual” operators
Proceedings of the Posters Workshop at CSD&M 2013 182
Towards a formal language for systemic requirements
[AI] [AS]
(x0 , , ), . . . input(x0 ) ( , q0 , ), . . . istate(q0 )
[AO] [e φ] ⇒ ⊥
( , , y0 ), . . . output(y0 ) e ¬φ
[AN]
e φ1 e φ2 e1 , e2 , . . . φ
[AW] [AC]
e φ1 ∧ φ2 , e1 , e2 , . . . φ
∃i ≤ 0, (ei , ei+1 , . . .) φ2 ∧ ∀k ∈ {0, . . . , i}, (ek , ek+1 , . . .) φ1
[AU]
e0 , e1 , . . . φ1 Uφ2
Definition 17 (system behaviour constraint). Let ∫ be a system. Let φ be
a P (∫ ) formula.
We say that ∫ satisfies φ, which is noted ∫ φ, iif
∀e ∈ exec(∫ ), e φ
In this case, φ is said to be a behaviour constraint on ∫ .
Example 2. Unsing our previous example 1, with θ⊥ = 15 and θ> = 20, here are
some behaviour constraints one would want to express on the system:
– ∫ ¬♦ istate(qof f ) ∧ output(heat)
– ∫ ¬♦ input(10) ∧ istate(qof f )
or, even more generally:
– ∀θ > θ> , ∫ ¬♦ input(θ) ∧ istate(qon )
3 Computation rules over behaviour constraints
We give here a minimalist set of computation rules to establish proofs about
system behaviours. A more advanced set of rules might be needed to ease such
proofs.
Proposition 1 (Product of two systems). Let ∫1 = (T, X1 , Y1 , Q1 , , , )
and ∫2 = (T, X2 , Y2 , Q2 , , , ) be two systems.
Let (x1 , x2 ) ∈ X1 × X2 , (y1 , y2 ) ∈ Y1 × Y2 and (q1 , q2 ) ∈ Q1 × Q2 .
∫1 input(x1 ) ∫2 input(x2 )
[PI]
∫1 ⊗ ∫2 input(x1 ⊗ x2 )
∫1 output(y1 ) ∫2 output(y2 )
[PO]
∫1 ⊗ ∫2 output(x1 ⊗ x2 )
Proceedings of the Posters Workshop at CSD&M 2013 183
Towards a formal language for systemic requirements
∫1 istate(q1 ) ∫2 istate(q2 )
[PS]
∫1 ⊗ ∫2 istate((q1 , q2 ))
Definition 18 (Composition of two systems). Let ∫1 = (T, X1 , Y1 , Q1 , , , )
and ∫2 = (T, X2 , Y2 , Q2 , , , ) be two systems such that Y1 = X2 .
We note ∫2 ◦ ∫1 the composition of ∫1 and ∫2 , obtained by “pluging” the output
of ∫1 to the input of ∫2 .
Proposition 2 (Composition of two systems). Let ∫1 = (T1 , X1 , Y1 , Q1 , , , )
and ∫2 = (T2 , X2 , Y2 , Q2 , , , ) be two systems such that T1 = T2 and Y1 = X2 .
Let (x, y, q1 , q2 ) ∈ X1 × Y2 × Q1 × Q2 ).
∫1 input(x)
[WI]
∫2 ◦ ∫1 input(x)
∫2 output(y)
[WO]
∫2 ◦ ∫1 output(y)
∫1 istate(q1 ) ∫2 istate(q2 )
[WS]
∫2 ◦ ∫1 istate((q1 , q2 ))
Conclusion
In this work we built a semantics of systems and provided a formal definition
of “properties” as timed behaviour constraints. The next step is to build a more
advanced refinement computation language that could let modelers obtain a
system from a set of such constraints.
References
1. LTL. http://en.wikipedia.org/wiki/Linear_temporal_logic. (last accessed on
31/10/2012).
2. O. Bournez and M.-L. Campagnolo. A survey on continuous time computations.
CoRR, abs/0907.3117, 2009.
3. B. Golden, M. Aiguier, and D. Krob. Modeling of complex systems ii: A minimalist
and unified semantics for heterogeneous integrated systems. Applied Mathematics
and Computation, 218(16):8039–8055, 2012.
4. B. Golden and Y. Hourdel. A minimalist formal framework for systems design.
2013.
5. T. A. Henzinger. The theory of hybrid automata. In Proceedings of the 11th Annual
IEEE Symposium on Logic in Computer Science, LICS ’96, pages 278–, Washington,
DC, USA, 1996. IEEE Computer Society.
6. D. Krob. Éléments de systémique - architecture des systèmes. 2012.
Proceedings of the Posters Workshop at CSD&M 2013 184