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.
ERCIM FMICS Home Page,
GMD FOKUS Home Page
Last modified: Wednesday, 19-Apr-2000 08:57:51 MET DST,
Axel Rennoch