Catálogo de publicaciones - libros

In this paper we present an attempt to represent dynamic communication links between abstract machines in the B method. The approach complements a previously proposed extension to B, that supports dynamic creation and deletion of machine instances, providing a mechanism for dynamically connecting or disconnecting machine instances for communication. This mechanism is based on the concept of connector , in the software architectures sense. We propose an extension to B’s notation to support the definition of connectors. The extension has been defined with the intention of making it fully compatible with the standard B method, and allows one to enable communication, under certain restrictions, between abstract machines in a specification which presents dynamic creation and deletion of machine instances. We present the extension, its semantics and an example illustrating its use based on a producer-consumer specification. We also discuss possible ways of extending the proposed connector definitions to more general forms of communication.

Despite the widespread use of the Transmission Control Protocol (TCP) as the main transport protocol in the Internet, the procedures for connection establishment and release are still not fully understood. This paper extends the analysis of a Coloured Petri net model of TCP’s Connection Management procedures by applying the state explosion alleviation technique known as the sweep-line method. The protocol is assumed to be operating over a reordering lossless channel. Termination and absence of deadlock properties are investigated for many scenarios, including client-server and simultaneous connection establishment, orderly release and abortion. The sweep-line method provides a reduction in memory usage of around a factor of 10 and allows investigation of many scenarios that were previously out of the reach of conventional methods.

Interface automata is a light-weight formalism to be used for describing the temporal interface behaviors of software components. This paper investigates the refinement of interface automatons and shows its application to serve as a semantic foundation for software architectural description languages. Firstly, inspired by 2/3 simulation, the 2/3 alternating simulation between interface automaton is presented, and the corresponding refinement relation is also derived between interface automaton. The distinguished feature is that it can preserve deadlock-freedom . Then, a concise formal semantics is provided for the architectural description language Wright , based on interface automaton, where the checking of compatibility and deadlock-freedom becomes simpler.

Telecommunicating systems should have a high degree of availability, i.e., high probability of correct and timely provision of requested services. To achieve this, correctness of software for such systems should be ensured. Application of formal methods helps us to gain confidence in building correct software. However, to be used in practice, the formal methods should be well integrated into existing development process. In this paper we propose a formal model-driven approach to development of communicating systems. Essentially our approach formalizes Lyra – a top-down service-oriented method for development of communicating systems. Lyra is based on transformation and decomposition of models expressed in UML2. We formalize Lyra in the B Method by proposing a set of formal specification and refinement patterns reflecting the essential models and transformations of Lyra. The proposed approach is illustrated by a case study.

We present a theoretically sound and automated model-based design, analysis, and implementation framework for synthesizing correct-by-construction code. Special emphasis is put on multi-threaded software and multi-processor architectures. The framework consists in (1) a formal language which provides platform-independent constructs to specify the behavior of an application using an abstract execution model, and (2) a compilation chain for refining the application abstract model into its concrete implementation on a target platform. The prototype Jahuel is currently being used for developing experimental industrial applications.

In this paper, we present a formal modeling and refinement approach for on-chip communication architecture development, based on the Action Systems formalism. Stepwise refinement from an abstract high-level initial model to an implementable parallel switch based model is discussed. The focus is on gradually decomposing the initial specification into a composition of concurrently operating subsystems. Data transactions are modelled with atomic message passing events via interface procedures, for which a new notation is introduced. The concept is demonstrated by a network-like pipelined bus platform.

Traditional network simulators perform well in evaluating the performance of network protocols but lack the capability of verifying the correctness of protocols. To address this problem, we have extended the J-Sim network simulator with a model checking capability that explores the state space of a network protocol to find an execution that violates a safety invariant. In this paper, we demonstrate the usefulness of this integrated tool for verification and performance evaluation by analyzing two widely used and important network protocols: AODV and directed diffusion. Our analysis discovered a previously unknown bug in the J-Sim implementation of AODV. More importantly, we also discovered a serious deficiency in directed diffusion. To enable the analysis of these fairly complex protocols, we needed to develop protocol-specific search heuristics that guide state-space exploration. We report our findings on discovering good search heuristics to analyze network protocols similar to AODV and directed diffusion.

Random Testing is a strategy to select test cases based on pure randomness. Adaptive Random Testing (ART), a family of algorithms, improves pure Random Testing by taking common failure pattern into account. The best—in terms of the number of test cases necessary to detect the first failure—ART algorithms, however, are too runtime inefficient. Therefore, a modification of a fast, but not so good ART algorithm, namely ART by Bisection, is presented. This modification requires much less test cases than the original method while retaining its computational efficiency.

In formal testing, the assumption of input enabling is typically made. This assumption requires all inputs to be enabled anytime. In addition, the useful concept of quiescence is sometimes applied. Briefly, a system is in a quiescent state when it cannot produce outputs. In this paper, we relax the input enabling assumption, and allow some input sets to be enabled while others remain disabled. Moreover, we also relax the general bound M used in timed systems to detect quiescence , and allow different bounds for different sets of outputs. By considering the tioco _ M theory, an enriched theory for timed testing with repetitive quiescence , and allowing the partition of input sets and output sets, we introduce the mtioco $_{\mathcal{M}}$ relation. A test derivation procedure which is nondeterministic and parameterized is further developed, and shown to be sound and complete wrt mtioco $_{\mathcal{M}}$ .

This paper presents a formal verification with the Coq proof assistant of a memory model for C -like imperative languages. This model defines the memory layout and the operations that manage the memory. The model has been specified at two levels of abstraction and implemented as part of an ongoing certification in Coq of a moderately-optimising C compiler. Many properties of the memory have been verified in the specification. They facilitate the definition of precise formal semantics of C pointers. A certified OCaml code implementing the memory model has been automatically extracted from the specifications.