Humboldt University Berlin, Dept. of Computer Science
Formal Description of SDL'92 Semantics using Extended Petri Nets
Diese Seite gibt es auch in Deutsch:
An analysis of SDL specifications is always to be accomplished taking into account certain specific target criteria such as :
- correctness proof (general/specific verification) and
- performance evaluation.
A decisive base for most different analysing and evaluating methods is the existence of a formal defined semantics of SDL, which guarantees an unambiguous interpretation of specifications of this language. A long-range objective of a semantics description of SDL using modified Petri Net calculus is the development of net based software tools for verification of SDL specifications regarding:
- deadlocks
- non reachable states
- reproducible states
Based on the powerfulness of the SDL semantics the following extensions are undertaken opposite to the classical Petri Net:
- attachment of data structures to some net places and
- attachment of time aspects (firing intervals) and preconditions (guard functions) to transitions.
With the help of these extensions it is possible to model and to describe effectively significant aspects of SDL specifications as: local process variables and signal parameters, the process input buffer management, the dynamic creation of process instances as well as the time behaviour of channels and timers.
A computer based investigation of real SDL specifications is possible by integration of existing and still to be developed analysing methods into the SDL Integrated Tool Environment SITE. The analysis of the automatically generated net modells using the reachability graph (RG) corresponds to the so called exhaustive simulation and it can by used as a proof for the correctness of the investigated specification. For the successful RG analysis a significant preposition is its finiteness. The principles of net analysis and of the corresponding tool are represented in the following figure:
The transformation of a SDL'92 specification into a corresponding net model (fig.2) as well as the transformation of the results back to the SDL level remain unvisible to the user. He has the illusion of investigation his own SDL specification. Because of this the consistent interpretation of the net analysis results within the original SDL world has a certain meaning. Following restrictions of SDL'92 have to be taken into account:
- no open parameters for process instance sets and only signal input buffer with a final capacity is permitted
- context parameters are not supported
- only SDL standard types are to be used.
The practical relevance of our approach was proved on two application examples: the Inres Protocol and the Sliding Window Protocol.
The further works concern:
- the complete implementation of transformation step T2
- reduction/elimination of the restrictions regarding to the SDL'92 language and
- development and implementation of additional net analysis algorithms (e.g. for determining place/transition invariants or algorithms for analysing of net models using suitable temporal logics)
edimitro@informatik.hu-berlin.de
Created at 03-07-96, last change at 03-07-96
