From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.1.3 Received: from discorde.inria.fr (discorde.inria.fr [192.93.2.38]) by yquem.inria.fr (Postfix) with ESMTP id 3F658BC69 for ; Mon, 10 Sep 2007 14:01:49 +0200 (CEST) Received: from hydra.cs.vu.nl (hydra.cs.vu.nl [130.37.16.4]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l8AC1mfI020695 for ; Mon, 10 Sep 2007 14:01:49 +0200 Received: from localhost (localhost [127.0.0.1]) by hydra.cs.vu.nl with esmtp (Smail #115) id m1IUhxc-0012q6C; Mon, 10 Sep 2007 14:01 +0200 Date: Mon, 10 Sep 2007 14:01:48 +0200 (CEST) From: Wan Fokkink To: caml-list@inria.fr Subject: Book announcement: Modelling Distributed Systems Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=X-UNKNOWN Content-Transfer-Encoding: QUOTED-PRINTABLE X-Miltered: at discorde with ID 46E5322C.002 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; algebra:01 algebra:01 syntax:01 semantics:01 abstraction:01 author's:01 rewriting:01 conditionals:01 transitions:01 branching:01 bounded:01 invariants:01 branching:01 bisimulation:01 model:01 I am delighted to announce that a new textbook is ready to preorder: Modelling Distributed Systems by Wan Fokkink Springer-Verlag, November 2007 ISBN 978-3-540-73937-1 For more information... www.springer.com/west/home?SGWID=3D4-102-22-173751350-0&changeHeader=3Dtr= ue&SHORTCUT=3Dwww.springer.com/978-3-540-73937-1 For extra material (slides, labs)... http://www.cs.vu.nl/~wanf/books.html COVER BLURB: A distributed system is driven by separate components that are executed in = parallel, and protocols for such systems form a major aspect of system design in toda= y's world of wireless and mobile networking. Process algebras are languages for the d= escription of elementary parallel systems and are used to study the behavioural proper= ties of distributed systems, but they often lack the ability to handle data. This textbook guides students through algebraic specification and verificat= ion of distributed systems, and some of the most prominent formal verification tec= hniques. The author employs =B5CRL as the vehicle, a language developed to combine p= rocess algebra and abstract data types. Chapters 2 and 3 explain the basics of abstract da= ta types and process algebra, and guide the reader through the syntax and semantics of = =B5CRL; Chap. 4 examines abstraction from internal behaviour; Chap. 5 covers specifications= of standard protocols; Chap. 6 shows how to transform protocol specifications into labe= lled transition systems; Chap. 7 explains algorithms on labelled transition syst= ems; and Chap. 8 presents symbolic verification techniques; finally, the Appendix gi= ves a brief overview of the =B5CRL toolset. The book evolved from introductory courses on protocol verification taught = to undergraduate and graduate students of computer science, and the text is su= pported throughout with examples and exercises; full solutions are provided in an a= ppendix, while exercise sheets, lab exercises, example specifications and lecturer s= lides will be available on the author's website. Researchers in the field can use the = book as a broad overview of the state of the art in algebraic specification and verif= ication of distributed systems on the basis of a modern verification tool. TABLE OF CONTENTS Introduction Abstract Data Types - Algebraic Specification - Term Rewriting - Equality Functions - Induction Process Algebra - Actions - Alternative and Sequential Composition - Parallel Processes - Deadlock and Encapsulation - Process Declarations - Conditionals - Summation over a Data Type - An Example: The Bag - Renaming - Bisimilarity Hiding Internal Transitions - Hiding of Actions - Summary - An Example: Two One-Bit Buffers in Sequence - Branching Bisimilarity Protocol Specifications - Alternating Bit Protocol - Bounded Retransmission Protocol - Sliding Window Protocol - Tree Identify Protocol - Movable Patient Support for an MRI Scanner Linear Process Equations - Linearisation - State Space Generation and Storage - CL-RSP - Invariants Verification Algorithms on State Spaces - Minimisation Modulo Branching Bisimulation - Confluence - Model Checking - Abstraction Symbolic Methods - Cones and Foci - Verification of the Tree Identify Protocol - Partial Order Reduction - Elimination of Parameters and Sum Variables - Symbolic Model Checking The =B5CRL Toolset in a Nutshell