Catálogo de publicaciones - libros

We present a graphical MSC-based representation of the language , which is a formal language for the description of Internet applications.

Some confusing Message Sequence Charts are identified, that can be considered as syntactically correct, but may lead to ambiguous interpretations. The first kind of MSC identified appears when parallel componentsof a parallel frame synchronize implicitly to continue an execution. The second case is called non-local choice, and appears when more than one instance is responsible for a choice. Non-local choice has already been studied before. This paper provides an extension of the definitions and corresponding detection algorithms. The third case is confluent MSCs, and appears when concurrency is expressed through a choice.

Message Sequence Charts (MSCs) is a visual notation for expressing requirements on communicating systems. Their expressive ower has traditionally been somewhat limited, and additional information is usually needed by tools that manipulate them: for example, to derive test suites. The new standard MSC-2000, developed by ITUT, extends earlier versions by constructs for data and high-level control, so that it may be possible to derive test sequences directly from MSC requirements, without the need for additional information. Motivated by this, we present an execution semantics for a significant part of the MSC-2000 standard. The semantics has the form of an Abstract Execution Machine, which can either accept or generate sequences of events that are consistent with a givenMSC. Inthe former case, the Abstract ExecutionMac hine canb e used as a test oracle, inthe latter as a test sequence generator.

This paper presents a comparison of four algorithms for test derivation: TorX, TGV, Autolink and UIO algorithms. The algorithms are classified according to the detection power of their conformance relations. Because Autolink does not have an explicit conformance relation, a conformance relation is reconstructed for it. The experimental results obtained by applying TorX, Autolink, UIO and TGV to the Conference Protocol case study are consistent with the theoretical results of this paper.

In this paper we propose a methodology for model-checking based verification of large SDL specifications. The methodology is illustrated by a case study of an industrial medium-access protocol for wireless ATM. To cope with the state space explosion, the verification exploits the layered and modular structure of the protocol’s SDL specification and proceeds in a bottom-up compositional way. To make a compositional approach feasible in practice, we develop a technique for losing SDL components with a chaotic environment without incurring the state-space penalty of considering all possible combinations of values in the input queues. The compositional arguments are used in combination with abstraction techniques to further reduce the state space of the system. With debugging the system as the prime goal of the verification, we corrected the specification step by step and validated various untimed and time-dependent properties until we built and verified a model of the whole control component of the medium-access protocol. The significance of the case study is in demonstrating that verification tools can handle complex properties of a model as large as shown.

Verification of operating procedures (that is, specifications of manual control actions) by model checking has been discussed in [16]. The modelling language Promela and the model checker Spin were used in that report. In order to be able to apply model checking in a wider scope, modelling languages with graphical interface and verification tools usedin industrial context are preferable (for example, to facilitate collaboration with process experts). In this paper, we discuss how to use SDL to model systems consisting of operating procedures and the controlled processes. Verification of procedures against correctness specifications is done by using the tool SDT. We conclude the paper with a short discussion of the integration of formal verification with the procedure design process.