Transcript Smart Cards Personalisation Machine in UPPAAL

Smart Card Personalisation
Machine in UPPAAL
Cybernetix case study for AMETIST project
Tomas Krilavičius & Yaroslav Usenko
Outline
Informal description
UPPAAL model
General description of model
Comparison with SMV model
Model
Demo
Tested configurations
Results
List of experiments
Result of experiments
Plans
Conclusions
Tomas Krilavičius & Yaroslav Usenko
Smart Card Personalisation Machine in UPPAAL
2
Informal description
CYBERNETIX Case Study, Informal
description
Sarah ALBERT, Cybernetix Recherche
Smart Card Personalisation Machine in SMV,
AMETIST: Cybernetix Case Study
Biniam GEBREMICHAEL, Frits VAANDRAGER, University of Nijmegen
Smart Card Personalisation Machine
Smart card personalisation machine takes a pile of the blank smart cards
as a raw material, programs them with the personalised data, prints them
and tests them.
Objectives
Synthesis of correct and optimal schedules
Model&tool for Cybernetix
Tomas Krilavičius & Yaroslav Usenko
Smart Card Personalisation Machine in UPPAAL
3
UPPAAL model
Simplified configuration
Conveyor
Unloader/Loader
Personalisation stations
Several versions
Chronological ordering by unloader
Chronological ordering by personalisation stations
Configurable parameters
conveyor length
number and positions of personalisation stations
temporal aspects: personalisation time, conveyor speed, unload/load time
Standard UPPAAL (timed automata with extensions)
Tomas Krilavičius & Yaroslav Usenko
Smart Card Personalisation Machine in UPPAAL
4
Comparison with SMV model
Smart Card Personalisation Machine in SMV, AMETIST:
Cybernetix Case Study
Biniam GEBREMICHAEL, Frits VAANDRAGER, University of Nijmegen
Both models are very abstract models
Differences
SMV model
UPPAAL model
Conveyor moves all the time
Conveyor can stop
Chronological ordering is
done by
personalisation stations
Chronological ordering is
done by
loader
personalisation stations
No unloading/loading time
Unloading/loading time
Tomas Krilavičius & Yaroslav Usenko
Smart Card Personalisation Machine in UPPAAL
5
Conveyor:
belt and conveyor movement
int[0,2*CARDS] c[CELLS] - the conveyor belt, where
CELLS is the length of the conveyor belt, (0..CELLS-1)
CARDS – the number of the cards in the batch (1..CARDS –
unpersonalised cards, CARDS+1..2*CARDS – personalised)
Tomas Krilavičius & Yaroslav Usenko
Smart Card Personalisation Machine in UPPAAL
6
Unloader:
Tomas Krilavičius & Yaroslav Usenko
unloads the cards on the conveyor one by one
Smart Card Personalisation Machine in UPPAAL
7
Loader:
removes the cards from the conveyor one by one
Tomas Krilavičius & Yaroslav Usenko
Smart Card Personalisation Machine in UPPAAL
8
Personalisation station
Tomas Krilavičius & Yaroslav Usenko
Smart Card Personalisation Machine in UPPAAL
9
Demonstration on UPPAAL
Tomas Krilavičius & Yaroslav Usenko
Smart Card Personalisation Machine in UPPAAL 10
Tested configurations
Chronological ordering
by unloader
by personalisation stations
Number of personalisation stations and cards in the batch
2 personalisation stations, 2..8 cards
3 personalisation stations, 2..6 cards
4 personalisation stations, 2..5 cards
Timing information
personalisation time = 10 time units
unloading/loading time = 2 time units
one conveyor step = 1 time unit
Tomas Krilavičius & Yaroslav Usenko
Smart Card Personalisation Machine in UPPAAL
11
Results: Experiments list
personalisation = 10, unloading/loading = 2 time units, conveyor step = 1
Cards
Stations
2
2
3
4
5
6
7
8
20
28
32
39
43
50
54
21
25
30
34
38


22
27
30
35



(4 cells)
3
(5 cells)
4
(6 cells)
Tomas Krilavičius & Yaroslav Usenko
Smart Card Personalisation Machine in UPPAAL 12
Results:
2 stations, 6 cards and 3 stations, 5 cards
Step
Station
1
1
2
1
Step
Station
1
1
2
3
1\1
2
3
4
2
Tomas Krilavičius & Yaroslav Usenko
5
4
6
3
2
3\2
2
6
5
3
4
4
\4
5
\5
\3
5
Smart Card Personalisation Machine in UPPAAL 13
Results: 4 stations
4 cards and 5 cards
Step
Station
1
1
1
2
2
3
3
2
3
4
4
Step
Station
1
1
1
2
2
2
3
4
5
5
3
4
4
3
Tomas Krilavičius & Yaroslav Usenko
4
Smart Card Personalisation Machine in UPPAAL 14
Interpretation of results
Unloading/loading stations are bottlenecks – the cards
should be spread to get better results
If unloading/loading is instant, the “super single mode”
and the “batches” algorithms are both “optimal”
Several schedules can be optimal; to find the scheduling
algorithm it would be useful to have tools, which allow to
get all optimal traces
Tomas Krilavičius & Yaroslav Usenko
Smart Card Personalisation Machine in UPPAAL 15
Plans
Models with more stations and more cards, several
batches of cards
Models with bi-directional conveyor
Models with
Graphical personalisation stations
Testing & reject stations
Flip over stations
Specialised versions of UPPAAL
Other tools
Tomas Krilavičius & Yaroslav Usenko
Smart Card Personalisation Machine in UPPAAL 16
Conclusions:
early stage
Smart card personalisation machine
Different abstractions of the system can be made
A fixed benchmark configuration is desirable to compare the results
More information about the system would be useful
UPPAAL
It is possible to model the system in UPPAAL
For small numbers of stations and cards it is possible to find optimal
schedules automatically
For automatic analysis of larger systems additional features could be
useful
diagnostic information (number of states, precise run-time information)
batch mode
access to the underlying transition system
guided search
question: is UPPAAL a right tool to model such systems (discrete time
systems, deterministic systems)
Tomas Krilavičius & Yaroslav Usenko
Smart Card Personalisation Machine in UPPAAL 17
That’s all...
Tomas Krilavičius & Yaroslav Usenko