Deriving schedules for a smart card personalisation system
Angelika Mader · University of Twente Research Information · 2004
We report on an industrial case study on the synthesis of (close) optimal schedules for a smart card personalisation system. The basic technique used is model checking. In most cases, the pure model checking approach has to be enriched by other techniques to fight the state space explosion. Other techniques can consist in adding additional knowledge about a system (discarding "useless" behaviour), or heuristics, or guiding model checking (priced model checking). In this case study we use decomposition as additional technique. We demonstrate the approach and discuss its generalizability.