Deriving Schedules for a Smart Card Personalisation System

    Research output: Book/ReportReportProfessional

    14 Downloads (Pure)


    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.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages15
    Publication statusPublished - Jan 2004

    Publication series

    NameCTIT Technical Report Series
    ISSN (Print)1381-3625


    • IR-48694
    • METIS-220406
    • EWI-799

    Cite this