Static Analysis by Abstract Interpretation of the Quasi Synchronous Composition of

Julien Bertrane

Description

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

Sujets

• Clock skew

Informations

• Publié par: pefav
• Publié le: 01 janvier 2005
• Nombre de lectures: 45
• Langue: English

Extrait

Static Analysis by Abstract Interpretation of
the Quasi-Synchronous Composition of
Synchronous Programs
Julien Bertrane, [e-mail]
´
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