Embedding Chaos

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 wellconsidered 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 statespace penalty in the input queues mentioned above. T...

• Type: Conference
• Year: 2001
• Where: SAS
• Authors: Natalia Sidorova, Martin Steffen
• Keywords: Formal Methods, Model Checking, Open Systems, SAS 2001, State-space Explosion Problem