//img.uscri.be/pth/46ae4d61e96cc2dd45317fa870a3148f5fdaeacf
Cet ouvrage fait partie de la bibliothèque YouScribe
Obtenez un accès à la bibliothèque pour le lire en ligne
En savoir plus

Static Analysis by Abstract Interpretation of the Quasi Synchronous Composition of

De
45 pages
Static Analysis by Abstract Interpretation of the Quasi-Synchronous Composition of Synchronous Programs Julien Bertrane, Ecole Normale Superieure, Paris, France VMCAI'05, 17 Janvier 2005 1

  • quasi-synchronous composition

  • normale superieure

  • synchronous programs

  • clock

  • allowing clock

  • duration between

  • modeling synchronous

  • clock skew


Voir plus Voir moins

Static Analysis by Abstract Interpretation of
the Quasi-Synchronous Composition of
Synchronous Programs
Julien Bertrane, bertrane@di.ens.fr
´
Ecole Normale Sup´erieure, Paris, France
VMCAI’05, 17 Janvier 2005
1Certification of embedded systems
Synchronous
System 1
Synchronous
System 2
Synchronous
System 3
wires (hardware)
computation (software)
– goal : Fault tolerance properties
Static Analysis by AI of the Quasi-Synchronous Composition of Synchronous Programs 2Modeling synchronous systems
– Synchronous systems :
– Initialize(S)
– while true do
– (O, S) := Compute (S, I)
– wait for clock
– od
where I : inputs, S : state variables, O : outputs
Static Analysis by AI of the Quasi-Synchronous Composition of Synchronous Programs 3Hypotheses for this model
– Quasi-synchrony :
– Each “synchronous” system is executed according to a
clock
– Clock Skew : Duration between two clock ticks belongs
to [α,β],α > 0.
– Serial transmission between synchronous systems
– A one-value buffer store data waiting to be read
– Initialisation of data to 0 or false according to its type.
Static Analysis by AI of the Quasi-Synchronous Composition of Synchronous Programs 4Difficulties
– Allowing clock imprecision (i.e. quasi-synchronous instead
of synchronous) enables non countable different behaviors
Synchronous
system δ−ε,δ+ε
I O
1 1
Xor
Synchronous
system δ−ε,δ+ε
?
Static Analysis by AI of the Quasi-Synchronous Composition of Synchronous Programs 5Plan
– Model : syntax and semantics
– Abstraction
– Analysis
– Simplification of concrete properties
– From concrete properties to abstract properties
– An example of analysis
Static Analysis by AI of the Quasi-Synchronous Composition of Synchronous Programs 6Syntax
Intuitive description Formal model
x z
z(t):=
DISCR DELAY − SHIFT
x
x(t−3)−y’(t) z 2.,2. 3.,3. 2.,2.
y:=x
SHIFT DISCR
2.,2.
2.,2. 2.,2.
y y’ y y’
transmission
DELAY DELAY
0< <2
delay 0.,2. 0.,2.
z’(t):= DISCR SHIFT
1.,3. 1.,3.
x’(t−3)−y(t)
x’ z’
x’ z’
y’:=x’
DISCR DELAY − SHIFT
1.,3. 3.,3. 1.,3.
1.,3.
Static Analysis by AI of the Quasi-Synchronous Composition of Synchronous Programs 7Modeling embedded systems
– Continuous-time semantics
which maps each point of control to a set of signals
(R7→B).
– Easy translation from synchronous frameworks, like
SCADE, to this syntax.
Static Analysis by AI of the Quasi-Synchronous Composition of Synchronous Programs 8Syntax and equational semantics of diagrams
Syntax equational semantics
O
1
+
I
1 ∀t∈R ,O (t) = I (t)
1 1
+
∀t∈R ,O (t) = I (t)
2 1
O
2
I
1
O
1
+
Or
∀t∈R ,O (t) = I (t) Or I (t)
1 1 2
I
2
+
CONST
∀t∈R ,O (t) = α
α 1
∀t∈R,O (t) = I (δ(t))
1 1

I O
1 1

DELAY
∃δ :R→R,monotonic,
[α,β]
δ :

∀t∈R,δ(t)−t∈ [α,β]
Static Analysis by AI of the Quasi-Synchronous Composition of Synchronous Programs 9Syntax and equational semantics of diagrams
I O
1 1
DISCR
[α,β]
For any clock c satisfying [α,β],
i.e. : c −c ∈ [α,β]
n+1 n


• 0



if t < c(0)
C C C C C C C C
O (t) =
1 2 3 4 5 6 7 8
1
 • I (c )
α
1 n



β
if t∈ [c ,c )
n n+1
Static Analysis by AI of the Quasi-Synchronous Composition of Synchronous Programs 10