Catálogo de publicaciones - libros

In this paper we investigate the connection between fragments of associative-commutative Term Rewriting and fragments of Mobile Ambients, a powerful model for mobile and distributed computations. The connection can be used to transfer decidability and undecidability results for important computational properties like reachability from one formalism to the other. Furthermore, it can be viewed as a vehicle to apply tools based on rewriting for the simulation and validation of specifications given in Mobile Ambients.

We are interested in black-box conformance testing of real-time systems. Our framework is based on the model of timed automata with inputs and outputs (TAIO). We use a timed conformance relation called tioco which is the extension of the untimed relation ioco. We show that considering only lazy-input TAIO is enough for describing all possible non-blocking specifications. We compare between tioco and the trace-inclusion relation. We prove that tioco is undecidable and that it does not distinguish specifications with the same set of observable traces. We prove tioco to be transitive and stable w.r.t both compositionality and action hiding for input-complete specifications. We compare between tioco and two other timed conformance relations, rtioco and .

Model checking of real-time systems with respect to Duration Calculus (DC) specifications requires the translation of DC formulae into automata-based semantics. This task is difficult to automate. The existing algorithms provide a limited DC coverage and do not support compositional verification. We propose a translation algorithm that advances the applicability of model checking tools to real world applications. Our algorithm significantly extends the subset of DC that can be handled. It decomposes DC specifications into sub-properties that can be verified independently. The decomposition bases on a novel distributive law for DC. We implemented the algorithm as part of our tool chain for the automated verification of systems comprising data, communication, and real-time aspects. Our translation facilitated a successful application of the tool chain on an industrial case study from the European Train Control System (ETCS).

This paper presents an automatic verification method for combined temporal and spatial properties of mobile real-time systems. We provide a translation of the Shape Calculus (SC), a spatio-temporal extension of Duration Calculus, into weak second order logic of one successor (WS1S). A prototypical implementation facilitates successful verification of spatio-temporal properties by translating SC specifications into the syntax of the WS1S checker MONA. For demonstrating the formalism and tool usage, we apply it to the benchmark case study “generalised railroad crossing” (GRC) enriched by requirements inexpressible in non-spatial formalisms.

This tutorial is proposed by representatives of the MeFoSyLoMa group. MeFoSyLoMa is an informal group gathering several teams from various universities in the Paris area:

– Université Paris-Dauphine (LAMSADE laboratory),

– Université P. & M. Curie (LIP6 laboratory),

– Université Paris 13 (LIPN laboratory),

– ENST (LTCI laboratory),

– Conservatoire National des Arts et Métiers (CEDRIC laboratory).

These teams have extensive knowledge and experience in the design, analysis and implementation of distributed systems. The cooperation within the group aims at joining forces, sharing experiences and building joint projects to solve issues in the design of reliable distributed systems.

Catching bugs in programs is difficult and time-consuming. The effort of debugging and proving correct even small units of code can surpass the effort of programming. Bugs inserted while “programming in the small” can have dramatic consequences for the consistency of a whole software system as shown, e.g., by viruses which can spread by exploiting buffer overflows, a bug which typically arises while coding a small portion of code. To detect this kind of errors, many verification techniques have been put forward such as static analysis and model checking.