introduction to the case study    
Informal description   Sarah Albert
Smart Card Personalisation Machine in SMV

additional material

Biniam Gebremichael and Frits Vaandrager
Smart Card Personalisation Machine in UPPAAL

powerpoint demo
(september 2002 meeting)
UPPAAL model (ta-format)
UPPAAL model (xml-format)

Tomal Krilavicius and
Yaroslav Usenko
Branch and Bound in Spin (december2002 meeting)
powerpoint demo
Theo Ruys
On Optimal Schedules (december2002 meeting)
powerpoint demo

(may 2003 meeting)

powerpoint demo
Angelika Mader
Towards Cost-Driven Uppaal

basic model
(no heuristics)

do 4 cards  
model with heuristics do 6 cards -oE (old tuppaal)
same model for new tuppaal do 6 cards -oE (new tuppaal)
Angelika Mader
The Cybernetix case study in mCRL

Initial muCRL model

An adaptation of the model to conform to the models of T. Krilavisius (UPPAAL) and T. Ruys (SPIN)

A model similar to cyber_tt.mcrl but has a finite underlying transition system

Slides from the meeting in Cassis 05-2003.

Yaroslav S. Usenko