Deriving Schedules for a Smart Card Personalisation System

Research output: Book/ReportReportProfessional

8 Downloads (Pure)

Abstract

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
No.04-05
ISSN (Print)1381-3625

Keywords

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

Cite this

Mader, A. H. (2004). Deriving Schedules for a Smart Card Personalisation System. (CTIT Technical Report Series; No. 04-05). Enschede: Centre for Telematics and Information Technology (CTIT).
Mader, Angelika H. / Deriving Schedules for a Smart Card Personalisation System. Enschede : Centre for Telematics and Information Technology (CTIT), 2004. 15 p. (CTIT Technical Report Series; 04-05).
@book{8f24301d195b4818b7517d29a06fe5ad,
title = "Deriving Schedules for a Smart Card Personalisation System",
abstract = "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.",
keywords = "IR-48694, METIS-220406, EWI-799",
author = "Mader, {Angelika H.}",
note = "Imported from DIES",
year = "2004",
month = "1",
language = "Undefined",
series = "CTIT Technical Report Series",
publisher = "Centre for Telematics and Information Technology (CTIT)",
number = "04-05",
address = "Netherlands",

}

Mader, AH 2004, Deriving Schedules for a Smart Card Personalisation System. CTIT Technical Report Series, no. 04-05, Centre for Telematics and Information Technology (CTIT), Enschede.

Deriving Schedules for a Smart Card Personalisation System. / Mader, Angelika H.

Enschede : Centre for Telematics and Information Technology (CTIT), 2004. 15 p. (CTIT Technical Report Series; No. 04-05).

Research output: Book/ReportReportProfessional

TY - BOOK

T1 - Deriving Schedules for a Smart Card Personalisation System

AU - Mader, Angelika H.

N1 - Imported from DIES

PY - 2004/1

Y1 - 2004/1

N2 - 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.

AB - 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.

KW - IR-48694

KW - METIS-220406

KW - EWI-799

M3 - Report

T3 - CTIT Technical Report Series

BT - Deriving Schedules for a Smart Card Personalisation System

PB - Centre for Telematics and Information Technology (CTIT)

CY - Enschede

ER -

Mader AH. Deriving Schedules for a Smart Card Personalisation System. Enschede: Centre for Telematics and Information Technology (CTIT), 2004. 15 p. (CTIT Technical Report Series; 04-05).