Paper Info
Title
Synchronous Closing of Timed SDL Systems for Model Checking
Abstract
Standard model checkers cannot handle open reactive systems directly. Closing the system is commonly done by adding an environmental process. 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 because of a combinatorial explosion caused by all combinations of messages in the input queues.In this paper we investigate a class of environmental processes for which the asynchronous communication scheme can safely be replaced by a synchronous one. Such a replacement is possible only if the environment is constructed under rather a severe restriction on the behavior, which can be partially softened via the use of a discrete-time semantics. We employ data-flow analysis to detect instances of variables and timers influenced by the data passing between the system and the environment.
Year
DOI
Venue
2002
10.1007/3-540-47813-2_6
VMCAI
Keywords
Field
DocType
data-flow analysis,open reactive system,model checking sdl,model checking,timed sdl systems,combinatorial explosion,environmental process,state-space explosion problem,asynchronous communication scheme,discrete-time semantics,standard model,synchronous closing,discrete time,reactive system,asynchronous communication,data flow analysis,message passing
Specification language,Asynchronous communication,Preemption,Programming language,Model checking,Computer science,Open system (systems theory),Reactive system,Combinatorial explosion,Semantics,Distributed computing
Conference
ISBN
Citations 
PageRank 
3-540-43631-6
3
0.45
References 
Authors
12
2
Name
Order
Citations
PageRank
Natalia Sidorova165754.08
Martin Steffen212210.32