Séminaire VASY 2011
Autrans (Isère)

Lundi 28 Novembre 2011

Déjeuner

14h30 – 15h40

Xavier Blanc (LaBRI)

Vpraxis et évolution d'application Internet

Pratiquement toutes les applications s'exécutent aujourd'hui sur Internet, quel que soit leur usage et quel que soit leur domaine. Une application qui s'exécute sur Internet fait partie d’un réel écosystème d'applications. Elle utilise et propose des ressources (donnée et/ou traitement) qui forment l'écosystème. Ces ressources, qui étaient il y a quelques années encore du simple texte, des images ou des vidéos, sont aujourd'hui beaucoup plus complexes, tels que des données sémantiques ou des services web par exemple.

Cette complexité croissante fait que le développement des applications Internet, et donc de l'écosystème, ne peut plus se faire par des équipes bien structurées, maîtres des artefacts logiciels qu'elles produisent et appliquant des cycles de développement traditionnels. Nous soutenons que le développement d'application Internet doit nécessairement prendre en considération le concept d'écosystème logiciel. Les applications de demain seront de plus en plus dépendantes de leur écosystème. Sans une forte réactivité de développement face aux évolutions de l’écosystème, une application deviendra vite dépassée et donc inutilisable ou extrêmement coûteuse en maintenance.

Le thème Sphere du LaBRI (http://sphere.labri.fr) développe l'approche VPraxis qui vise à contrôler l'évolution des applications Internet. Notre objectif est de modéliser les histoires des différents composants des applications Internet afin de contrôler leur interdépendance. Cette présentation portera sur VPraxis et montrera le modèle qu'il propose afin de modéliser l'évolution d'un écosystème logiciel.

15h40 – 16h25

Hubert Garavel (joint work with the VASY team)

CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes

CADP (Construction and Analysis of Distributed Processes) is a comprehensive software toolbox that implements the results of concurrency theory. Started in the mid 80s, CADP has been continuously developed by adding new tools and enhancing existing ones. Today, CADP benefits from a worldwide user community, both in academia and industry. This paper presents the latest release CADP 2010, which is the result of a considerable development effort spanning the last five years. The paper first describes the theoretical principles and the modular architecture of CADP, which has inspired several other recent model checkers. The paper then reviews the main features of CADP 2010, including compilers for various formal specification languages, equivalence checkers, model checkers, performance evaluation tools, and parallel verification tools running on clusters and grids.

Pause café

16h50 – 17h50

Wendelin Serwe (joint work with the VASY team)

LNT and its translation to LOTOS

In this talk, we present LOTOS NT (abbreviated LNT), the principal input language of CADP. After a presentation of the language, we also overview its implementation in CADP, namely by translation into LOTOS.

Dîner

Mardi 29 Novembre 2011

9h10 – 10h35

Christian Attiogbé (LINA)

Composition dynamique de processus dans les systèmes complexes

L'interaction entre les composants d'un système distribué peut être modélisée par la composition adéquate des composants. Ainsi, la modélisation et l'étude des systèmes reposent en grande partie sur la composition parallèle des composants. Dans de nombreux systèmes, il y a de plus en plus de facteurs qui complexifient l'interaction entre les composants : production/transport de données, mobilité, mutation de type, hétérogénéité, architecture ad hoc, etc.

Les composants et les systèmes qui les intègrent évoluent donc du point de vue des fonctionnalités et des comportements et aussi vis-à-vis de leur environnement, et cela doit être prévu dans leurs modèles. La modélisation des systèmes et leur vérification demeurent ainsi des défis à relever.

Nous étudions la composition dynamique de processus représentant des composants d'un système distribué, comme un moyen de maîtriser la modélisation et la correction de systèmes complexes. La composition dynamique s'appuie sur une approche événementielle qui intègre les données, les processus / comportements et les événements. Les idées et les exemples sont ici expérimentés en Event-B, mais transposables aux algèbres de processus.

10h35 – 11h20

Frédéric Lang (joint work with Pepijn Crouzen)

Smart Reduction

Compositional aggregation is a technique to palliate state explosion – the phenomenon that the behaviour graph of a parallel composition of asynchronous processes grows exponentially with the number of processes – which is the main drawback of explicit-state verification. It consists in building the behaviour graph by incrementally composing and minimizing parts of the composition modulo an equivalence relation. Heuristics have been proposed for finding an appropriate composition order that keeps the size of the largest intermediate graph small enough. Yet the underlying composition models are not general enough for systems involving elaborate forms of synchronization, such as multiway and/or nondeterministic synchronizations. We overcome this by proposing a generalization of compositional aggregation that applies to an expressive composition model based on synchronization vectors, subsuming many composition operators. Unlike some algebraic composition models, this model enables any composition order to be used. We also present an implementation of this approach within the CADP verification toolbox in the form of a new operator called smart reduction, as well as experimental results assessing the efficiency of smart reduction.

Pause café

11h40 – 12h30

Radu Mateescu

MCL in a Nutshell

MCL (Model Checking Language) is an extension of the alternation-free modal mu-calculus with regular expressions over transition sequences, data-handling primitives, and fairness operators. Although it was initially designed from a verification perspective to enhance the expressiveness and user-friendliness of temporal logic specifications, MCL can be seen as a language for querying labeled transition systems (LTSs). In this talk, we will present MCL using examples of increasingly complex properties allowing the characterization of various subgraphs (sequences, trees, cycles, lassos, etc.) contained in an LTS. We briefly describe the model checking procedure for MCL implemented in the EVALUATOR 4.0 tool of CADP, discuss the relation of MCL with classical temporal logics, and indicate future research directions.

12h30 – 13h30

Hubert Garavel (with contributions of Susanne Graf)

Three decades of success stories in formal methods

We present the results of a recent bibliographic study to identify significant results of formal methods research. Over the period 1982-2011, we have decided to identify one key contribution per year, so that 30 contributions in total are reviewed in this talk.

Déjeuner

16h30 – 17h20

Frédéric Lang (joint work with Radu Mateescu)

Partial Model Checking using Networks of Labelled Transition Systems and Boolean Equation Systems

Partial model checking was proposed by Andersen in 1995 to verify a temporal logic formula compositionally on a composition of processes. It consists in incrementally incorporating into the formula the behavioural information taken from one process --- an operation called quotienting --- to obtain a new formula that can be verified on a smaller composition from which the incorporated process has been removed. Simplifications of the formula must be applied at each step, so as to maintain the formula at a tractable size. In this paper, we revisit partial model checking. First, we extend quotienting to the network of labelled transition systems model, which subsumes most parallel composition operators, including m among n synchronisation and parallel composition using synchronization interfaces, available in the E-LOTOS standard. Second, we reformulate quotienting in terms of a simple synchronous product between a graph representation of the formula (called formula graph) and a process, thus enabling quotienting to be implemented efficiently and easily, by reusing existing tools dedicated to graph compositions. Third, we propose simplifications of the formula as a combination of bisimulations and reductions using Boolean equation systems applied directly to the formula graph, thus enabling formula simplifications also to be implemented easily and efficiently. Finally, we describe an implementation in the CADP (Construction and Analysis of Distributed Processes) toolbox and present some experimental results in which partial model checking uses hundreds of times less memory than on-the-fly model checking.

Pause café

17h45 – 18h30

Wendelin Serwe (joint work with Etienne Lantreibecq)

Model Checking and Co-simulation of a Dynamic Task Dispatcher Circuit using CADP

The complexity of multiprocessor architectures for mobile multi-media applications renders their validation challenging. In addition, to provide the necessary flexibility, a part of the functionality is realized by software. Thus, a formal model has to take into account both hardware and software. In this paper we report on the use of LOTOS NT and CADP for the formal modeling and analysis of the DTD (Dynamic Task Dispatcher), a complex hardware block of an industrial hardware architecture developed by STMicroelectronics. Using LOTOS NT facilitated exploration of alternative design choices and increased the confidence in the DTD, by, on the one hand, automatic analysis of formal models easily understood by the architect of the DTD, and, on the other hand, co-simulation of the formal model with the implementation used for synthesis.

18h30 – 19h10

Gwen Salaün (joint work with Xavier Etchevers, Noël De Palma, Fabienne Boyer, and Thierry Coupaye)

Verification of a Self-configuration Protocol for Distributed Applications in the Cloud

Distributed applications in the cloud are composed of a set of virtual machines running a set of interconnected software components. In this context, the task of automatically configuring distributed applications is a very difficult issue. In this talk, we focus on such a self-configuration protocol, which is able to configure a whole distributed application without requiring any centralized server. The high degree of parallelism involved in this protocol makes its design complicated and error-prone. In order to check that this protocol works as expected, we specify it in LOTOS NT and verify it using the CADP toolbox. The use of these formal techniques and tools helped to detect a bug in the protocol, and served as a workbench to experiment with several possible communication models.

19h10 – 19h50

Matthias Güdemann

Qualitative and Quantitative Formal Model-Based Safety Analysis

The key aspect of model-based methods is a common system model which is shared between different people working on the development of the system.

In this work, the model-based approach is combined with failure-injection techniques to allow more accurate safety analysis than possible before. A system is not considered in isolation, but as a combination of SW / HW, its physical environment and possible erroneous behavior of components.

The approach allows a sound combination of both qualitative and qualitative analysis methods. It is based on a formal modeling language which allows non-deterministic and probabilistic behavior, proven correct and complete analysis methods, support for different types of probabilistic failure modes and model-transformations into the input languages of different verification tools.

Dïner

Mercredi 30 Novembre 2011

9h00 – 10h10

Grégory Batt (INRIA/Contraintes – joint work with Aurélien Rizk, François Fages, and Sylvain Soliman)

A general computational method for robustness analysis with applications to synthetic gene networks

Robustness is the capacity of a system to maintain a function in the face of perturbations. It is essential for the correct functioning of natural and engineered biological systems. Robustness is generally defined in an ad hoc, problem-dependent manner, thus hampering the fruitful development of a theory of biological robustness, recently advocated by Kitano. In this work, we propose a general definition of robustness that applies to any biological function expressible in temporal logic LTL (linear temporal logic), and to broad model classes and perturbation types. This notion relies on a quantitative interpretation of temporal logic on numerical traces. We propose a computational approach and an implementation in BIOCHAM 2.8 for the automated estimation of the robustness of a given behavior with respect to a given set of perturbations. The applicability and biological relevance of our approach is demonstrated by testing and improving the robustness of the timed behavior of a synthetic transcriptional cascade that could be used as a biological timer for synthetic biology applications.

10h10 – 10h50

Radu Mateescu (joint work with Anton Wijs)

Property-Dependent Reductions for the Modal Mu-Calculus

When analyzing the behavior of finite-state concurrent systems by model checking, one way of fighting state explosion is to reduce the model as much as possible whilst preserving the properties under verification. We consider the framework of action-based systems, whose behaviors can be represented by labeled transition systems (LTSs), and whose temporal properties of interest can be formulated in modal mu-calculus (Lmu). First, we determine, for any Lmu formula, the maximal set of actions that can be hidden in the LTS without changing the interpretation of the formula. Then, we define dsbrLmu, a fragment of Lmu which is compatible with divergence-sensitive branching bisimulation. This enables us to apply the maximal hiding and to reduce the LTS on-the-fly using divergence-sensitive tau-confluence during the verification of any dsbrLmu formula. The experiments that we performed on various examples of communication protocols and distributed systems show that this reduction approach can significantly improve the performance of on-the-fly verification.

Pause café

11h15 – 11h50

Iker Bellicot (joint work with Radu Mateescu)

Massively Parallel Resolution of Boolean Equation Systems

Boolean Equation Systems (BESs) are a useful formalism enabling the reformulation of various problems in the field of concurrent systems analysis (model checking, equivalence checking, partial order reduction, etc.). The resolution of very large BESs, produced from the verification of complex systems, requires a large amount of computing resources. In this talk we present a distributed BES resolution algorithm that runs on several machines connected by a network. The algorithm has been implemented in the BES_SOLVE tool of CADP, which is dedicated to the benchmarking and testing of BES resolution algorithms on BESs represented as textual files or generated randomly according to various parameters. We illustrate the performance of the distributed algorithm on several benchmarks executed on Grid5000.

11h50 – 12h35

Gwen Salaün (joint work with Tevfik Bultan and Nima Roohi)

Realizability of Choreographies using Process Algebra Encodings

Service-oriented computing has emerged as a new software development paradigm that enables implementation of Web accessible software systems that are composed of distributed services which interact with each other via exchanging messages. Modeling and analysis of interactions among services is a crucial problem in this domain. Interactions among a set of services that participate in a service composition can be described from a global point of view as a choreography. Choreographies can be specified using specification languages such as Web Services Choreography Description Language (WS-CDL) and visualized using graphical formalisms such as collaboration diagrams.

In this talk, we present an encoding of collaboration diagrams into the LOTOS process algebra for choreography analysis. This encoding allows us to (i) check the temporal properties of choreographies using a LOTOS verification tool set called the Construction and Analysis of Distributed Processes (CADP) toolbox, (ii) check the realizability of choreographies for both synchronous communication and asynchronous communication, and (iii) automate the peer generation process.

Realizability indicates whether peers can be generated from a given choreography specification in such a way that the interactions of the generated peers exactly match the choreography specification. If a collaboration diagram is unrealizable, our approach extends the peer generation process by adding extra communication that guarantees that the peers behave according to the choreography specification.

Déjeuner

Visite de la ferme de la Bourrière (Méaudre) puis départ à Grenoble vers 15h30