Models and Analysis for Distributed Systems

Serge Haddad, Fabrice Kordon, Laurent Pautet, Laure Petrucci, Serge Haddad, Fabrice Kordon, Laurent Pautet, Laure Petrucci

• Publisher: Wiley-ISTE
• Year: 2013
• Print ISBN: 9781848213142
• eBook ISBN: 9781118602683
• Edition: 1
• Topic: Computer Science
• Subtopic: Computer Engineering
• Index: Computer Science

Nowadays, distributed systems are increasingly present, for public software applications as well as critical systems. software applications as well as critical systems. This title and Distributed Systems: Design and Algorithms – from the same editors – introduce the underlying concepts, the associated design techniques and the related security issues.
The objective of this book is to describe the state of the art of the formal methods for the analysis of distributed systems. Numerous issues remain open and are the topics of major research projects. One current research trend consists of profoundly mixing the design, modeling, verification and implementation stages. This prototyping-based approach is centered around the concept of model refinement.
This book is more specifically intended for readers that wish to gain an overview of the application of formal methods in the design of distributed systems. Master's and PhD students, as well as engineers in industry, will find a global understanding of the techniques as well as references to the most up-to-date works in this area.

Chapter 1

Introduction ¹

Problematics

The complexity of dynamic systems grows much faster than our ability to manage them [LEV 97]. In particular, the parallel execution of the threads of a distributed system requires the elaboration of sophisticated models and methods.

The oldest technique, simulation, is a straightforward way to increase confidence about the correctness of an implementation. Such a simulation is based on a model of the system with operational semantics in order to perform the elementary steps of the system. Unfortunately due to the non-determinism of distributed systems, replaying a simulation is a difficult task.

More precisely this problem is a consequence of two factors: the variable transit time of any message and the relative speed of the machine processors. Thus with the help of (vectorial) logical clocks associated with every station, additional information can be managed during the simulation so that it can be replayed [BON 96]. Such mechanisms can easily be integrated within a framework for distributed execution (called middleware).

Even if simulation techniques point out some bugs, they can never fully reassure to the designer of the system. Thus tests must be combined with other techniques in order to obtain a more complete validation of the system.

Among these alternative approaches, the more efficient ones are associated with the early stage of the design. The most appropriate method consists of equipping the design step with a formal model such as UML¹ [CHA 05]. Unfortunately UML is not intended to have an operational semantic and this feature is required for the analysis of distributed systems. In particular, a formal semantic for the component behavior and for their composition is essential in view of checking the properties of the system.

Once a model with a formal semantics is obtained, the properties can be expressed either in a specific way (absence of deadlocks, mutual exclusion, etc.) or in a generic way via some logic (such as temporal logics) that can express fairness, liveness, etc. Furthermore, in order to combine performance evaluation, and verification, quantitative logics have also been introduced.

There are also difficulties with verification methods [LUQ 97]: the competency of the designer, the adaption to industrial case studies, the ability to tackle large-scale applications. Thus pragmatism is a key factor in the success of formal methods: without tools and methodology formal methods would never be adopted by engineers [KOR 03].

Objective of this book

The objective of this book is to describe the state of the art in formal methods for distributed and cooperative systems. These systems are characterized by:

– several components with one or more threads, possibly running on different processors;

– asynchronous communications with possible additional assumptions (reliability, order preserving, etc.);

– or local view for every component and no shared data between components.

These are the most common features in modern distributed systems. Numerous issues remain open and are the topic of European research projects. One current research trend consists of intricately mixing the design, modeling, verification, and implementation stages. This prototyping-based approach [KOR 03] is centered around the concept of refinement of models.

This book is more specifically intended for readers who wish to get an overview of the application of formal methods in the design of distributed systems. Master’s and PhD students, and engineers will obtain a thorough understanding of the techniques as well as references for the most up-to-date work in this area.

Organization of the book

This book follows the two stages of a formal method: modeling, and verification.

Part 1 is concerned with the initial step of system design: modeling.

– Chapter 3 discusses a modeling approach to design a consistent specification. After identifying the key elements of the system to be modeled, they are step by step taken into account, and refined until the model is obtained.

– Chapter 4 is devoted to efficient handling of time. Timed models address mechanisms to manipulate time within distributed systems. They make use of discrete clocks and variables, while hybrid systems consider continuous evolution of time.

– Chapter 5 is concerned with the description of software architectures using dedicated languages that are ADLs (architecture description languages).

Part 2 is concerned with the next step of system design: verification.

– Chapter 7 covers the finite-state verification. Historically it is the oldest line of research that has been developed. The main objective of finite-state verification is the reduction of complexity due to the combinatory explosion of the system. Possible approaches are structural methods, which try to avoid developing the behavior of the system, and data representation which reduces the explosion by sharing substructures or exploiting the properties satisfied by the formalism.

– Chapter 8 addresses the problem of verifying infinite-state systems. Most of the research is devoted to the design of formalisms, which are slightly less expressive than Turing machines (or equivalent computational models), and to study which properties are decidable. In this chapter, the main focus is put on extensions of Petri nets and on different variants of counter machines. It emphasizes the fact that small variations lead to drastically different theories.

– Chapter 9 studies timed systems. Time is a particular source of infinity. However, its specificity leads to efficient verification procedures such as those developed for timed automata. Moreover, time can be combined with other sources of infinity such as in time(d) Petri nets. In addition, this chapter tackles the problem of implementing timed systems when the abstractions achieved at the theoretical level (such as the perfect synchronization of the clocks) are no longer satisfied.

– Chapter 10 studies control and synthesis of distributed systems. After recalling the centralized case, it develops, with the aid of specific examples, the specifics of the distributed case and the different possible approaches.

The MeFoSyLoMa community

MeFoSyLoMa (Méthodes Formelles pour les Systèmes Logiciels et Matériels² ) is 0an association gathering several world-renowned research teams from various laboratories in the Paris area [MEF 11]. It is composed of people from LIP6³ (P. & M. Curie University), LIPN ⁴ (University of Paris 13), LSV⁵ (École Normale Supérieure de Cachan), LTCI⁶ (Telecom ParisTech), CÉDRIC⁷ , (CNAM), IBISC⁸ (University of Évry-Val-d’Esssone), and LACL⁹ (University of Paris 12). Its members, approximately 80 researchers and PhD students, all have common interest in the construction of distributed systems and promote a software development cycle based on modeling, analysis (formal), and model-based implementation. This community was founded in 2005 and is federated by regular seminars from well-known researchers (inside and outside the community) as well as by common research activities and the organization of events in their domains such as conferences, workshops, or book writing.

The editors of this book, as well as most authors, are from this community.

Bibliographie

[BON 96] BONNAIRE X., BAGGIO A., PRUN D., “Intrusion Free Monitoring: An Observation Engine for Message Server Based Applications”, 9th International Conference on Parallel And Distributed Computing Systems (ISCA), p. 88-93, 1996.

[CHA 05] CHARROUX B., OSMANI A., THIERRY-MIEGY., Eds., UML2, Pearson Education, 2005.

[KOR 03] KORDON F., HENKEL J., “An overview of Rapid System Prototyping today”, Desig...

Table of contents

• Cover
• Title Page
• Copyright
• Foreword
• Chapter 1: Introduction
• FIRST PART: Formal Models for Distributed Systems
• SECOND PART: Verification Techniques for Distributed Systems
• List of Authors
• Index