Static Analysis by Abstract Interpretation of the Quasi Synchronous Composition of

pages

English

Documents

2005

Écrit par
Julien Bertrane

Publié par
pefav

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

pages

English

Ebook

2005

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Publié par

pefav

Publié le

01 janvier 2005

Nombre de lectures

Langue

English

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

Publié par

pefav

Publié le

01 janvier 2005

Nombre de lectures

Langue

English

Clock skew

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
1Certiﬁcation 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 buﬀer 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 4Diﬃculties
– Allowing clock imprecision (i.e. quasi-synchronous instead
of synchronous) enables non countable diﬀerent 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
– Simpliﬁcation 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