Embedding chaos

N. Sidorova, M. Steffen

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

7 Citations (Scopus)

Abstract

Model checking would answer all finite-state verification problems, if it were not for the notorious state-space explosion problem. A problem of practical importance, which attracted less attention, is to close open systems. Standard model checkers cannot handle open systems directly and closing is commonly done by adding an environment process, which in the simplest case behaves chaotically. However, for model checking, the way of closing should be well-considered to alleviate the state-space explosion problem. This is especially true in the context of model checking SDL with its asynchronous message-passing communication, since chaotically sending and receiving messages immediately leads to a combinatorial explosion caused by all combinations of messages in the input queues. In this paper we develop an automatic transformation yielding a closed system. By embedding the outside chaos into the system’s processes, we avoid the state-space penalty in the input queues mentioned above. To capture the chaotic timing behaviour of the environment, we introduce a non-standard 3-valued timer abstraction. We use data-flow analysis to detect instances of chaotic variables and timers and prove the soundness of the transformation, which is based on the result of the analysis.
Original languageEnglish
Title of host publicationStatic Analysis (Proceedings 8th International Symposium, SAS 2001, Paris, France, July 16-18, 2001)
EditorsP. Cousot
Place of PublicationBerlin
PublisherSpringer
Pages319-334
ISBN (Print)3-540-42314-1
DOIs
Publication statusPublished - 2001

Publication series

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

Fingerprint Dive into the research topics of 'Embedding chaos'. Together they form a unique fingerprint.

Cite this