Catálogo de publicaciones - libros

Despite the increasing need of formal methods, people in the industry still hesitate to use them for product development because they are not sure of success with that novel approach in their own situation. In order to encourage those people we show our experience of designing a radio resource control protocol for ETRI’s 3G evolution systems in SDL with two different approaches: pure-SDL and hybrid-SDL approaches. From our design and verification results, we make an empirical evaluation of those two approaches in several aspects and suggest a simple guideline for selecting an appropriate approach according to the situation.

Creating and maintaining tools for domain-specific modeling languages (DSML) demands time and efforts that often discourage potential developers. However, several tools are now available that promise to accelerate the development of DSML environments. In this paper, we evaluate five such tools (GME, Tau G2, RSA, XMF-Mosaic, and Eclipse with GEF and EMF) by observing how well they can be used to create graphical editors for the Goal-oriented Requirement Language (GRL), for which a simplified metamodel is provided. We discuss the evaluation criteria, results, and lessons learned during the creation of GRL editors with these technologies.

The User Requirements Notation (URN) combines the Goal-oriented Requirement Language (GRL) with the Use Case Map (UCM) scenario notation. Although tools exist in isolation for both views, they are currently not meant to work together, hence preventing one to exploit URN to its fullest extent. This paper presents , a new Eclipse-based tool that supports both UCM and GRL in an integrated way. jUCMNav supports links between the two languages that can be exploited during analysis. An overview of the current editing and analysis capabilities is given, with a particular emphasis on the new concept of GRL , which simplify the evaluation of GRL models. The extensibility of the tool is also discussed.

ConTraST is a configurable C++ code generator that provides a mapping of SDL specifications in SDL/PR to an object oriented C++ representation. The transformation from one high level language to another allows the configuration of supported language features, giving the name: a configurable transpiler. The intention is to obtain the object oriented structure and thereby increase the readability and traceability of the generated code. This code is compiled together with an SDL runtime environment, which was derived by manually transforming the formal semantics of SDL-2000 standard Z.100 F.3 into C++ preserving both structure and behavior. This provides a continuous traceability from the SDL specification to the executing system including its runtime environment.