Paper Info
Title
Closing Open SDL-Systems for Model Checking with DTSpin
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.
Year
DOI
Venue
2002
10.1007/3-540-45614-7_30
FME
Keywords
Field
DocType
embedding chaos,external environment process,chaotic environment,closing open sdl-systems,environment process,combinatorial explosion,state space,model checking,separate process,case study,dtpromela translation,asynchronous message-passing communication,message passing,open system,reactive system,abstractions,communication system
Asynchronous communication,Model checking,Embedding,Computer science,Real-time computing,Theoretical computer science,Open system (systems theory),Reactive system,Combinatorial explosion,State space,Message passing,Distributed computing
Conference
ISBN
Citations 
PageRank 
3-540-43928-5
11
0.71
References 
Authors
19
3
Name
Order
Citations
PageRank
Natalia Ioustinova1626.99
Natalia Sidorova265754.08
Martin Steffen312210.32