Closing open SDL-systems for model checking with DTSpin
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.
|Design Tools and Techniques (acm D.2.2), Software/Program Verification (acm D.2.4), Languages (acm D.2.1.1), Model Validation and Analysis (acm I.6.4)|
|Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (msc 68N30), Semantics (msc 68Q55), Specification and verification (program logics, model checking, etc.) (msc 68Q60), Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (msc 68Q85)|
|Software Engineering [SEN]|
|Organisation||Specification and Analysis of Embedded Systems|
Ioustinova, N, Sidorova, N, & Steffen, M. (2002). Closing open SDL-systems for model checking with DTSpin. Software Engineering [SEN]. CWI.