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
closing open systems, since standard model checkers cannot handle
open systems. 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.
