Closing open SDL-systems for model checking with DTSpin

N. Ioustinova, N. Sidorova, M. Steffen

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

11 Citations (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.
Original languageEnglish
Title of host publicationFME2002: Formal methods - Getting IT Right (Proceedings International Symposium of Formal Methods Europe, Copenhagen, Denmark, July 22-24, 2002)
EditorsL.-H. Eriksson, P. Lindsay
Place of PublicationBerlin
ISBN (Print)3-540-43928-5
Publication statusPublished - 2002
EventInternational Symposium of Formal Methods Europe (FME 2002), July 22-24, 2002, Copenhagen, Denmark - Copenhagen, Denmark
Duration: 22 Jul 200224 Jul 2002

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


ConferenceInternational Symposium of Formal Methods Europe (FME 2002), July 22-24, 2002, Copenhagen, Denmark
Abbreviated titleFME 2002
Other"Formal methods - Getting IT Right"


Dive into the research topics of 'Closing open SDL-systems for model checking with DTSpin'. Together they form a unique fingerprint.

Cite this