5th International Workshop on

Formal Methods for Industrial Critical Systems

Berlin, April 3-4, 2000

A Practical Method to Integrate Abstractions into SDL and MSC based Tools

Many industrial oriented tools that employ SDL, as the basis to develop complex systems support very detailed specifications in order to perform tasks such as simulation, code generation or testing. But the size of the SDL model constructed for these purposes makes the verification of MSCs more resource confuming, due to the well-known problem of the state space explosion. This paper presents a proposal in the direction of optimising the verification ofMSCs without limiting the use of SDL in the other tasks. The main contribution of the paper is the defintion of a practical automatable method to obtain intermediate SDL specifications suitable for the efficient verification of MSCs. The correctness of the transformation is supported by the definition of a semantics framework that allows us to compare different SDL models of the same system, each one with a particular abstraction level.

Note: The content of the following files is part of GMD Report No. 91 and subject to its copyright.


Last modified: Wednesday, 19-Apr-2000 08:57:51 MET DST, Axel Rennoch