Catálogo de publicaciones - libros

We present here an ASM view and an SDL view of the same protocol. We show how the two different modeling paradigms complement each other and that they are similar in their underlying semantic models. Our application example is sufficiently complex, including both architectural as well as non-trivial algorithmic aspects, and overall addresses an interesting problem in a demanding technological sector.

Soft state signaling protocols install and maintain states in network nodes, expiring without receiving refreshes. These states require proper reparation when the flow path changes, especially in case of link or node failures. As the specifications usually do not describe in detail how to handle these failures, we present insights by developing SDL models for RSVP on this issue.

We have used SDL to support the design and implementation of SLACP, a novel logical link layer protocol to enhance the performance of TCP over wireless WAN links. The protocol was modeled in SDL and successive refinements of its design were carried out based on feedback obtained from using the validation facilities of Telelogic Tau 4.4 SDT.

This paper deals with mobility protocols specification, validation and testing using a formal approach. A well suited SDL model is proposed to handle the component-based nature of Mobile systems. Two solutions are proposed to derive automatically TTCN-3 test cases from the SDL model.

Cinderella SLIPPER is a C-code generator that generates C code from SDL and ASN.1 models defined in Cinderella SDL. The code generator has been designed to produce compact readable C code, as one of the major obstacles of using generated code from design specifications is that software developers are inhibited by difficulties to understand the generated code.

Ubiquitous computing and communications services are the focus of intense current research and development. These systems are essentially asynchronous reactive systems of independent agents. However, there is little evidence of recent use of visual formalisms like SDL in their development. This represents a challenge and an opportunity.

This paper presents ArchiTRIO (), a new temporal logic language which combines a subset of the UML notation with a precise formal semantics inspired from the authors’ experiences. ArchiTRIO allows developers to use standard UML 2.0 notation to describe non-critical aspects of systems, but it also offers a complementary formal notation, fully integrated with the UML one, to represent those system aspects that require precise modeling.

Despite their apparent simplicity, Web applications are surprisingly difficult to develop, if our aim is to build applications that behave correctly under regular conditions as well as adverse circumstances like out-of-order requests and race conditions. In this paper, we describe our experiences deriving customer-oriented acceptance tests for Web applications by modeling the essential capabilities of such applications with Use Case Maps (UCMs). Abstract test purposes are generated from a UCM model using scenario definitions and scenario extraction tools. These test purposes are then converted interactively to test cases in the FitNesse acceptance testing framework, which is popular in the Extreme Programming (XP) community. The test cases are used to validate a Web application where several typical but non-trivial bugs were planted. Challenges in the automation of the process are also discussed.

As testing often consumes over 40% of the typical project development effort, there is great need for optimizing the testing effort. In addition, as the cost of fixing defects is dramatically lower when fixing those close to where they were introduced, finding defects in the early life-cycle phases is critical. TTCN-3 (Testing and Test Control Notation), developed at ETSI and standardized by the ITU-T, enables testers to specify test cases for the various types of testing, and supports reuse of test artifacts. We have used TTCN-3 as a complete test solution in the development of network element software. This paper presents the benefits we have observed during system development and provides a comparison with other testing practices deployed in our organization.

This paper presents a validation approach that exploits the compositional properties of a system. Our results can be applied on systems modelled by state machines and asynchronous communication by message passing. We consider two axes of composition: horizontal composition across system components, and vertical composition within components. Along the horizontal axis, we reduce the complexity of validation analysis by using a projection technique that allows us to validate interactions between components pairwise. We further simplify by introducing a set of design rules that support the development of well-formed state machines. When these rules are enforced, we are able to apply a simplified compatibility checking algorithm. Along the vertical axis, validation is applied incrementally. Elementary component collaborations are validated first, then their composite.