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

10 Citations (Scopus)

Abstract

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
PublisherSpringer
Pages531-548
ISBN (Print)3-540-43928-5
DOIs
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
Volume2391
ISSN (Print)0302-9743

Conference

ConferenceInternational Symposium of Formal Methods Europe (FME 2002), July 22-24, 2002, Copenhagen, Denmark
Abbreviated titleFME 2002
CountryDenmark
CityCopenhagen
Period22/07/0224/07/02
Other"Formal methods - Getting IT Right"

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

Cite this