Closing open SDL-systems for model checking with DTSpin

N. Ioustinova, N. Sidorova, M. Steffen

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

11 Citaten (Scopus)


Model checkers like Spin can handle closed reactive systems, only. Thus to handle open systems, in particular when using assume-guarantee reasoning, we need to be able to close (sub-)systems, which is commonly done by adding an environment process. For models with asynchronous message-passing communication, however, modelling the environment as separate process will lead to a combinatorial explosion caused by all combinations of messages in the input queues. In this paper we describe the implementation of a tool which automatically closes DTPromela translations of SDL-specifications by embedding the timed chaotic environment into the system. To corroborate the usefulness of our approach, we compare the state space of models closed by embedding chaos with the state space of the same models closed with chaos as external environment process on some simple models and on a case study from a wireless ATM medium-access protocol.
Originele taal-2Engels
TitelFME2002: Formal methods - Getting IT Right (Proceedings International Symposium of Formal Methods Europe, Copenhagen, Denmark, July 22-24, 2002)
RedacteurenL.-H. Eriksson, P. Lindsay
Plaats van productieBerlin
ISBN van geprinte versie3-540-43928-5
StatusGepubliceerd - 2002
EvenementInternational Symposium of Formal Methods Europe (FME 2002), July 22-24, 2002, Copenhagen, Denmark - Copenhagen, Denemarken
Duur: 22 jul 200224 jul 2002

Publicatie series

NaamLecture Notes in Computer Science
ISSN van geprinte versie0302-9743


CongresInternational Symposium of Formal Methods Europe (FME 2002), July 22-24, 2002, Copenhagen, Denmark
Verkorte titelFME 2002
AnderInternational Symposium of Formal Methods Europe


Duik in de onderzoeksthema's van 'Closing open SDL-systems for model checking with DTSpin'. Samen vormen ze een unieke vingerafdruk.

Citeer dit