FORMAL METHODS FOR OPEN OB)ECT-BASED DISTRIBUTED SYSTEMS IV IFIP -The International Federation for Information Processing IFIP was founded in 1960 under the auspiees of UNESCO, following the First World Computer Congress held in Paris the previous year. An umbrella organization for societies working in information proeessing, IFIP's aim is two-fold: to support information proeessing within its member countries and to eneourage technology transfer to developing nations. As its mission statement clearly states, IFIP's mission is to be the leading, truly international, apolitieal organization whieh encourages and assists in the development, exploitation and applieation of information technology for the benefit of all people. IFIP is a non-profitmaking organization, run almost solely by 2500 volunteers. It operates through a number of technieal committees, whieh organize events and publieations. IFIP's events range from an international eongress to loeal seminars, but the most important are: • The IFIP World Computer Congress, held every second year; • open eonferenees; • working eonferenees. The flagship event is the IFIP World Computer Congress, at whieh both invited and contributed papers are presented. Contributed papers are rigorousIy refereed and the rejection rate is high. As with the Congress, partieipation in the open eonferenees is open to all and papers may be invited or submitted. Again, submitted papers are stringently refereed. The working conferences are structured differently. They are usually run by a working group and attendance is small and by invitation only. Their purpose is to ereate an atmosphere conducive to innovation and development. Refereeing is Iess rigorous and papers are subjeeted to extensive group diseussion. Publieations arising from IFIP events vary. The papers presented at the IFIP World Computer Congress and at open conferences are published as eonference proceedings, while the results of the working conferenees are often published as eolleetions of seleeted and edited papers. Any national society whose primary activity is in information may apply to beeome a full member of IFIP, although full membership is restrieted to one society per country. Full members are entitled to vote at the annual General AssembIy, National societies preferring a less committed involvement may appIy for assoeiate or corresponding membership. Associate members enjoy the same benefits as full members, but without voting rights. Corresponding members are not represented in IFIP bodies. Affiliated membership is open to non-national societies, and individual and honorary membership sehemes are also offered. FORMAL METHODS FOR OPEN OBJECT-BASED DISTRIBUTED SYSTEMS IV IFlP TC6/WG6.1 Fourth International Conference on Formal Methods for Open Objed-Based Distributed Systems (FMOODS 2000) September 6-8, 2000, Stanford, California, USA Edited by Scott F. Smith The lohns Hopkins University USA Carolyn L. Talcott Stanford University USA ~. " KLUWER ACADEMIC PUBLISHERS BOSTON / DORDRECHT / LONDON Distributors ror North, Central and South America: Kluwer Academic Publishers 101 Philip Drive Assinippi Park Norwell, Massachusetts 02061 USA Telephone (781) 871-6600 Fax (781) 871-6528 E-Mail <[email protected]> Distributors ror al1 other countries: Kluwer Academic Publishers Group Distribution Centre Post Office Box 322 3300 AH Dordrecht, THE NETHERLANDS Telephone 31 78 6392 392 Fax 31 78 6546474 E-Mail <[email protected] > ~. " E1ectronic Services <http://www.wkap.n1> Library of Congress Cataloging-in-Publication Data International Conference on Fonnal Methods for Open Object-Based Distributed Systems (4th: 2000 : Stanford, Calif.) Fonnal methods for open object-based distributed systems IV : IFIP TC6/WG6.1 Fourth International Conference on Fonnal Methods for Open Object-Based Distributed Systems (FMOODS 2000) : September 6-8, 2000, Stanford, California, USA 1 edited by Seott F. Smith, Carolyn L. Talcott. p. cm. - (International Federation for Infonnation Proeessing ; 49) Ineludes bibliographieal references. ISBN 978-1-4757-1018-2 ISBN 978-0-387-35520-7 (eBook) DOI 10.1007/978-0-387-35520-7 I. Electronic data processing-Distributed processing-Congresses. 2. Objeet oriented programming (Computer seienee)-Congresses. I. Smith, Seott F. 11. Talcott, Carolyn L. III. Title. IV. International Federation for Infonnation Proeessing (Series) ; 49. QA76.9.D5 1573 2000 005.1 '17-de21 00-056231 Copyright @ 2000 by International Federation for Infonnation Processing. Softcover reprint ofthe hardcover 1st edition 2000 All rights reserved. No part ofthis publication may be reprodueed, stored in a retrieval system or transmitted in any form or by any means, meehanical, photo-copying, recording, or otherwise, without the prior written permission of the publisher, Kluwer Academic Publishers, 101 PhiJip Drive, Assinippi Park, Norwell, Massachusetts 02061. Printed on acid-free paper. Contents Prefaee ix Part I Invited Talk On the Semantics of JavaSpaees 3 Nadia Busi, Roberto Gorrieri, Gianluigi Zavattaro Part n Mobility Elements of an object-based model for distributed and mobile eomputation 23 lean-Bemard Ste/ani, Florence Germain, Elie Najm Specifieation of Mobile Code Systems using Graph Grammars 45 Femando Lu(s Dotti, Leila Ribeiro Atomie Failure in Wide-Area Computation 65 Dominic Duggan rn Part Invited Talk Rewriting Logie and Maude: a Wide-Spectrum Semantie Framework for Object-Based Distributed Systems 89 lose Meseguer Part IV Java / UML Requirements Level Semanties for UML Statecharts 121 Rik Eshuis, Roel Wieringa A Step Toward Automatie Distribution of Java Programs 141 Isabelle Attali, Denis Caromel, Romain Guider vi Using Relational and Behavioural Semantics in the Verification of Object Models 163 Christie Bolton, lim Davies Formally Modeling UML and its Evolution: A Holistic Approach 183 Ambrosio Toval Alvarez, lose Luis Fernandez Aleman Part V Invited Talk Object-Oriented Programming for Wide-Area Computing 209 layadev Misra Part VI Refinement and Subtyping Behavioural Subtyping and Property Preservation 213 Heike Wehrheim A Practical Approach to Incremental Specification 233 Charles lAkos, Glenn Lewis Refinement of objects and operations in Object-Z 257 lohn Derrick, Eerke Boiten Part VII Invited Talk E-speak: the Technology for Ubiquitous E-services 281 AlanH. Karp Part VIII Time Behavior Expression and OMDD 285 Yunming Wang On a Temporal Logic for Object-Based Systems 305 Dino Distefano, loost-Pieter Katoen, Arend Rensink Stochastically Enhanced Timed Automata 327 Lynne Blair; Trevor lones, Gordon Blair Contents vii Part IX Components Fail-Stop Components by Pattern Matching 351 Tomasz Janowski, Wojciech I. Mostowski A Formal Specification of the CORBA Event Service 371 Remi Bastide, Ousmane Sy, David Navarre, Philippe Palanque Components as Processes: An Exercise in Coalgebraic Modeling 397 L S. Barbosa Preface This volume contains the proceedings of the Fourth IFIP WG 6.1 Inter national Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODSOO). The conference was held in Stanford, California, on September 6-8, 2000. The event was the fourth meeting of this conference series, initiated in Paris in March 1996. The goal of the FMOODS series of conferences is to bring together re searchers whose work encompasses three important and related fields: • formal methods, • distributed systems, and • object-based technology. Such a convergence is representative of some of the latest advances in the field of distributed systems and provides links between several scientific and technological communities (for instance, FORTEIPSTV, ICODP, ECOOP, etc.). The papers inc1uded in this book, which were presented at the conference, reflect the scope of the conference. The collection inc1udes abstracts or papers of several invited talks, and papers that were submitted, reviewed, and accepted by the Program Committee. Invited Speakers We were fortunate to have the following invited speakers at FMOODS 2000: • Roberto Gorrieri is Professor of Computer Science at the Universty of Bologna. His research interests inc1ude: theory of concurrency and co ordination, formal methods and security.He is member of the executive board of EATCS, secretary of IFIP Technical Committee 1, and chair of IFIP WG 1.7 on foundations of security analysis and design. • Jose Meseguer is a Principal Scientist at SRI International in Menlo Park, California. His reaserch interests inc1ude logic and semantics in com puter science, formal methods, programming languages, and concurrent computing. • Jayadev Misra is a professor and holder of the Regents' chair in the De partment of Computer Sciences at the Univ. of Texas at Austin. His x research interests are in the area of concurrent programming, with em phasis on rigorous methods to improve the programming process. Misra is a fellow of ACM and IEEE; he held the Guggenheim fellowship during 1988-1989. • Alan Karp is a Department Scientist in the Decision Technology Depart ment at HP Labs where he is conducting research in economic models for Internet economies. Before that, he was Senior Technical Contributor and Chief Scientist at Hewlett-Packard's E-speak Operation, the group responsible for bringing HP's e-speak technology to market. He was one of the architects of the HP/lntel iA64 processor. The technical papers in this volume inc1ude 16 papers that were selected among 33 submissions. The conference was partitioned in several sessions cov ering formal methods related to the following topics: mobility, Java and UML, refinement and subtyping, temporal and probablistic properties, and compo nents. The conference is sponsered by IFIP, in particular TC 6 and WG6.1, and thanks are due to Guy Leduc for his advice and support in this respect. We would like to thank the authors for their high quality submissions. We are very grateful to the program committee members and external referees for all their efforts in reviewing papers. SCOTI SMITH AND CAROLY N T ALCOTI BaZtimore and Stanford Committee members and list of referees CONFERENCE CHAIR Carolyn Talcott (Stanford University) PROGRAM COMMITTEE CHAIR Scott Smith (The Johns Hopkins University) PROG RAM COMMITTEE Gul Agha (U. of Illinois, USA) Patrick Bellot (ENST, Paris, France) Lynne Blair (U. Lancaster, UK) Howard Bowman (UKC, Kent, UK) Paolo Ciancarini (U. Bologna, ltaly) John Derrick (UKC, Kent, UK) Michel Diaz (LAAS-CNRS, Toulouse, France) Alessandro Fantechi (U. Firenze, ltaly) Kathleen Fisher (ATT Research Labs, USA) Kokichi Futatsugi (Jaist, Ishikawa, Japan) Joseph Goguen (UC San Diego, USA) Roberto Gorrieri (U. Bologna, ltaly) Guy Leduc (u. of Liege, Belgium) Luigi Logrippo (U of Ottawa, Canada) David Luckham (Stanford University, USA) Jan de Meer (GMD Fokus, Berlin, Germany) EHe Najm (ENST, Paris, France) Dusko Pavlovic (Kestrel Institute, USA) Omar Rafiq (U. of Pau, France) Arend Rensink (U. Twente, Netherlands) Sriram Sankar (Metamata Inc., USA) Gerd Schuermann (GMD Fokus, Berlin, Germany) Scott Smith (Johns Hopkins University, USA) Jean-Bemard Stefani (FT/CNET, Issy-les-Moulineaux, France) Carolyn Talcott (Stanford University, USA) Nalini Venkatasubramanian (UC Irvine, USA)