Science

Specification and Description Language (SDL) is used for designand specification of services especially in the field of telecommunications. It is standardized in the ITU-T Recommendation Z.100 and can be used from the abstract system design phase to the automated generation of implementations inthe chosen programming language.

In an ideal development environment each change in the specification of the product would be immediately formally checked against requirements specification. This is not an easy task. First, we have to choose one of theavailable formal verification techniques and tools that suit our needs. We use the Simple Promela Interpreter (Spin) model checker. Model checking is one of the most popular methods for automatic formal verification. To verify a real-life system it must be usually convertedinto a simpler ``verifiable'' format - the model of the (sub)system. Next, each requirement should be formally described in a way that developers fully understand its true meaning. If we use one of the temporal logics, this goal is not always easy to achieve. Finally, we check if the model satisfies the requirements. Formal verification techniques check all possible execution paths. If we have sound model of the system and correctly written requirement, the model checking will provide positive result or anexecution path that does not satisfy the requirement.

A model can be generated manually or mechanically. Manual preparation of a modelis error prone and very time consuming task. Therefore, our research focuses on automating model generation from SDL specification. The final research goal isto build a framework for the systematic use of model checking in the developing process of our industry partners. We focus on specifications that describethe implementation details and are used to build the production systems. Such specifications use SDL constructs and additional extensions that enable developers to include operators that are implemented in other programming languages. Our industry partners use programming language C for low-level or processor intensive operations. Therefore, the framework should support such extensions of the SDL.

After detailed study of existing techniques, we decided to propose a new approach to automated model generation from SDL to Process Meta Language(Promela) that is used by the Spin tool.

You can find more information in the selected publications or check out our tools.