IF Tutorial Marius BOZGA Susanne GRAF Iulian OBER Laurent MOUNIER VERIMAG Distributed and Comp le x Systems Group www-verimag.imag.fr/PEOPLE/async/IF/ SPIN work sh op IF Tut o rial 1 A p ril 2, 200 4 mot i vat i on – l anguage – tools
– c ase s t udies
- p erspectives model based development Goal Early detection of problems, concerning functional and non functional aspects model-based simulation, testing and verification Context Telecommunication protocols, Real-time embedded systems, Distributed systems, Scheduling problems,… SPIN work sh op IF Tut o rial 2 A p ril 2, 200 4mot i vat i on – l anguage – tools
– c ase s t udies
- p erspectives approach: build on the existing User level modeling and CASE tools (SDL, UML, SCADE, …) Translation to a intermediate language, rich enough for modeling and for validation Optimisation a nd abstraction state Semantic model (state graph) explosion simulation verification3 verification1 test verification2 SPIN work sh op IF Tut o rial 3 A p ril 2, 200 4mot i vat i on – l anguage – tools
– c ase s t udies
- p erspectives approach: build on the existing CADP LOTOS guarded commands Optimisation a nd abstraction Semantic model (state graph) simulation verification3 verification1 test verification2 SPIN work sh op IF Tut o rial 4 A p ril 2, 200 4mot i vat i on – l anguage – tools
– c ase s t udies
- p erspectives approach: build on the existing Kronos Timed automata Optimisation a nd abstraction Semantic ...
IF Tutorial
Marius BOZGA
Susanne GRAF
Iulian OBER
Laurent MOUNIER
VERIMAG
Distributed and Comp
le
x Systems Group
www-verimag.imag.fr/PEOPLE/async/IF/
SPIN work
sh
op
IF Tut
o
rial
1
A
p
ril 2,
200
4
mot
i
vat
i
on
–
l
anguage –
tools
–
c
ase s
t
udies
-
p
erspectives
model based development
Goal
Early detection of problems,
concerning functional and non
functional aspects
model-based simulation, testing
and verification
Context
Telecommunication protocols,
Real-time embedded systems,
Distributed systems,
Scheduling problems,…
SPIN work
sh
op
IF Tut
o
rial
2
A
p
ril 2,
200
4mot
i
vat
i
on
–
l
anguage –
tools
–
c
ase s
t
udies
-
p
erspectives
approach: build on the existing
User level
modeling and
CASE tools (SDL,
UML, SCADE, …)
Translation to a intermediate language,
rich enough for modeling and for validation
Optimisation
a
nd abstraction
state
Semantic model (state graph)
explosion
simulation
verification3
verification1
test
verification2
SPIN work
sh
op
IF Tut
o
rial
3
A
p
ril 2,
200
4mot
i
vat
i
on
–
l
anguage –
tools
–
c
ase s
t
udies
-
p
erspectives
approach: build on the existing
CADP
LOTOS
guarded commands
Optimisation
a
nd abstraction
Semantic model (state graph)
simulation
verification3
verification1
test
verification2
SPIN work
sh
op
IF Tut
o
rial
4
A
p
ril 2,
200
4mot
i
vat
i
on
–
l
anguage –
tools
–
c
ase s
t
udies
-
p
erspectives
approach: build on the existing
Kronos
Timed automata
Optimisation
a
nd abstraction
Semantic model (state graph)
verification2
verification1
SPIN work
sh
op
IF Tut
o
rial
5
A
p
ril 2,
200
4mot
i
vat
i
on
–
l
anguage –
tools
–
c
ase s
t
udies
-
p
erspectives
challenge
A good intermediate representation
•
S
ufficient
expressiveness
: allows to map
concepts of diverse modeling languages
(asynchronous, synchronous, timing,…)
•
E
nough
concepts
: structured representation of
–
C
oncepts existing in validation tools
–
C
oncepts exploitable for
more efficient validation
•
A
llows
semantic fine tuning
: allows expression of
alternative options of semantic variation points:
time progress, execution and interaction
modes,…
SPIN work
sh
op
IF Tut
o
rial
6
A
p
ril 2,
200
4overview
•
M
otivation and challenge
•
IF: the language concepts
–
F
unctional aspects
–
N
on-fu
n
ctional aspects
•
IF: the toolset
–
C
ore components
–
M
odel-based validation
–
F
ront-end tools
•
D
emos
•
Case studies
•
P
erspectives
SPIN work
sh
op
IF Tut
o
rial
7
A
p
ril 2,
200
4mot
i
vation –
language –
tools
–
c
ase s
t
udies
-
perspectives
perspectives
•
U
ML-based methodology for real-time systems
–
c
omponent-based
modeling
–
c
ombination
asynchronous
and
synchronous
syste
ms
–
r
elate
functional
and
non-functional
aspects
•
i
mprove verification and test generation methods
–
m
ore static analysis
,
abstraction
and constraint propagation
–
m
ore
compos
itional
verification methods
–
better
diagnostics
facilities
•
m
ore connections
–
c
onnections with
performance evaluation
tools
SPIN work
sh
op
IF Tut
o
rial
8
A
p
ril 2,
200
4The IF Language
Functional Part
SPIN work
sh
op
IF Tut
o
rial
1
A
p
ril 2,
200
4system
–
p
rocess
–
c
ommunic
a
tion –
example –
e
xtens
ions
IF Specification
System description : 3 axes
Processes
extended timed automata
IF
(non-determinism, dynamic creation)
predefined data types
(basic types, arrays,
Communications
records)
asynchronous channels
abstract data types
shared variables
Data
SPIN work
sh
op
IF Tut
o
rial
2
A
p
ril 2,
200
4