Catálogo de publicaciones - libros

Scenario-based specifications such as message sequence charts (MSCs) offer an intuitive and visual way of describing design requirements. As one powerful formalism, Petri nets can model concurrency constraints in a natural way, and are often used in modelling system specifications and designs. Since there are gaps between MSC models and Petri net models, keeping consistency between these two kinds of models is important for the success of software development. In this paper, we use Petri nets to model concurrent systems, and consider the problem of checking Petri nets for scenario-based specifications expressed by message sequence charts. We develop the algorithms to solve the following two verification problems: the existential consistency checking problem, which means that a scenario described by a given MSC must happen during a Petri net runs, or any forbidden scenario described by a given MSC never happens during a Petri net run; and the mandatory consistency checking problem, which means that if a reference scenario described by the given MSCs occurs during a Petri net run, it must adhere to a scenario described by the other given MSC.

SDL claims to be a language for the description of open systems, allowing the integration of other components into an SDL system and that of an SDL system as a mere component into a greater unit. Indeed, SDL provides the possibility for the interaction of a system with its environment. Signals can be exchanged with the environment and in addition the developer may hide arbitrary actions inside external procedures.

Code generators are widely in use to produce runnable code from an SDL system description, decreasing faults and increasing flexibility. But changes in or changes of the communication protocol to the environment still force a code generator to be adapted, costing precious resources.

This paper presents an automated code generation from SDL to C++, which enables the flexible connection of various communication protocols without changing the code generator or adding code manually. A runtime library contains all necessary means for communication to the environment, an approach which has been tested using CORBA and Web Services, but could be adapted easily to arbitrary protocols.

Problems with the choice of appropriate encodings seem to be solved with the recommendation Z.104, which enables the specification of encodings already in the SDL-2000 system. All results presented in this paper are based on the experience gained in practice during several projects using Cinderella SITE.

We present a tool that automatically checks the existence of a bisimulation relation between an SDL specification and the corresponding auto-generated C code. The tool has been used to verify part of the C implementation of a WiFi Medium Access Controller (IEEE 802.11) that has been derived from its original SDL specification using the Telelogic CAdvanced Code Generator.

Telecommunication services are provided as the joint effort of components, which collaborate in order to achieve the goal(s) of the service. UML 2.0 collaborations can be used to model services. Furthermore, they allow services to be described modularly and incrementally, since collaborations can be composed of subordinate collaborations. For such an approach to work, it is necessary to capture the exact dependencies between the subordinate collaborations. This paper presents the results of an experiment on using Use Case Maps (UCMs) for describing those dependencies, and for synthesizing the state-machine behaviour of service components from the joint information provided by the UML collaborations and the UCM diagrams.