Lecture Notes ni Computer Science detidE yb .G Goos dna .J Hartmanis 430 .W.J de Bakker W.-R de reveoR G. Rozenberg (Eds.) esiwpetS tnemenifeR fo detubirtsiD smetsyS ,sledoM ,smsilamroF ssentcerroC XER ,pohskroW ,kooM sdnalrehteN ehT yaM 29- ,2 enuJ 9891 sgnideecorP galreV-regnirpS grebledieH nilreB kroYweN nodnoL siraP oykoT gnoH gnoK Editorial Board D, Barstow W, Brauer .P Brinch Hansen D, Gries D. Luckham C, Moler A. Pnueli G. Seegm~ller .J Stoer N. Wirth Editors J.W. de Bakker Centre for Mathematics and Computer Science Kruislaan 413, 1098 SJ Amsterdam, The Netherlands W.-P. de Roever Department of Computing Science Eindhoven University of Technology P.O. Box 513, 5600 MB Eindhoven, The Netherlands G. Rozenberg Institute of Applied Mathematics and Computer Science University of Leiden P.O. Box 9512, 2300 RA Leiden, The Netherlands CR Subject Classification (1987): E3, D.1,3 ISBN 3-540-52559-9 Springer-Verlag Berlin Heidelberg New York ISBN 0-387-52559-9 Springer-Verlag NewYork Berlin Heidelberg work This sirights All copyright. to subject era ,devreser whether eht of part or whole eht lairetam of rights the specifically concerned, is ,noitalsnart illustrations, of re-use reprinting, ,noitaticer ,gnitsacdaorb on reproduction smliforcim ways, other in or dna egarots data in .sknab noitacilpuD thereof parts or publication this of si only dettimrep the under snoisivorp the of namreG Copyright waL of rebmetpeS 9, ,5691 June of version its in ,42 ,5891 copyright a and eef always must eb prosecution the under fall Violations paid. tca of eht Copyright German .waL © galreV-regnirpS Heidelberg Berlin 0991 in Printed ynamreG Beltz, Druckhaus binding: and Printing .rtsgreB/hcabsmeH paper acid-free on Printed 2145/3140-543210 - Preface The stepwise refinement method postulates a system construction route that starts with some relatively high-level specification, goes through a number of provably correct devel- opment steps, each of which replaces some declarative, non-executable (or merely ineffi- cient) aspects of the specification by imperative executable constructs, and ends with an (efficiently) executable program. In the past decade, this paradigm has generated an extremely active research area. The proceedings of this workshop are intended to survey the state of the art in this area, both from the theoretical and from the practical side. The following topics were discussed: Models: What are the features of a specification that may change during refinement and what features should be maintained? Trace based refinement concentrates on the sequences of system actions. Yet others maintain that the ability to make certain choices during computations should be maintained during refinement. Then again, maybe such decisions should follow from the interactions that are possible between systems. Other important topics are independence and interface refinement. Refinementn otions for dis- tributed systems should express that parts of such systems act independently and con- currently from each other. Also, during development not only a system's control changes but also a system's interface, e.g., an event may become a signal on a serial port. This is an extremely important topic that is only now starting to be addressed by researchers. Formalisms: What constitutes a good formalism to specify systems and their develop- ment? Much of the theoretical research has used various artificial programming languages. But, also the use of various forms of transition systems or automata has been proposed, and is becoming increasingly popular for specifying complicated systems. In that case, should one specify system behavior by giving the concrete automata that generate it or should one give such automata in a more abstract way, e.g. by specifying the possible transitions by assertional means. Other viable options are the use of temporal logic and of algebraic specifications as formalisms. Correctness: How is a program-developmenstt ep verified? The answer is to a large ex- tent determined by the formalism that is used and the refinement notion that is adopted. Much theoretical work has concentrated on equational axiomatizations of refinement no- tions, thus giving rise to calculi on program terms. Using automata engenders the use of simulation relations with which to prove refinement; a method which may come closer to the operational intuitions aonf implementor. Temporal logic-like formalisms need first or- der proof systems, while (equational) algebraic specifications make use of rewrite systems or theorem provers. The material presented in this volume was prepared after the workshop took place by the lecturers, their co-authors, and some of the observers -- in this way the results of the discussions during the workshop could be reflected in the proceedings. We are proud that we had such an excellent group of lecturers and we believe that this volume represents rather completely the state of the research in this field at the moment. We are very grateful to the lecturers and the other participants for making the workshop a scientific and social success. We wish to thank R. Gerth, A. Pnueli, R. van Glabbeek, E.-R. Olderog, C. Courcoubetis, and L. Lamport for their help in suggesting speakers and in defining the format of this workshop. Judging by the number of Dutch authors in the present volume and the quality of their contributions, in our own opinion this volume demonstrates that the extra funding by the Dutch Government of computer science in the Netherlands in general, and of the field of concurrency in particular, is bearing fruit. We gratefully acknowledge the financial support fl'om our funding agency, the Netherlands National Facility for Informatics (NFI). We thank the Eindhoven University of Technology for the technical organisation of the workshop and its financial support. We want to extend our special thanks to E. van Thiel-Niekoop and A. Smulders for their organisational assistance, and to Ron Koymans and Kees Huizing for taking the burden of the local organisation upon their shoulders at late notice. We believe that it is no coincidence that the participants were boarded in Hotel de Plasmolen and Hotel de Molenhoek; the Dutch word "molenm"e ans mill, one of mankind's earliest refinement devices. March 0991 The editors J.W. de Bakker W.P. de Roever G. Rozenberg The REX project The REX Research and Education in Concurrent Systems -- project investigates -- syntactic, semantic and proof-theoretic aspects of concurrency. In addition, its objectives are the education of young researchers and, in general, the dissemination of scientific results relating to these themes. REX is a collaborative effort of the Leiden University (G. Rozenberg), the Centre for Mathematics and Computer Science in Amsterdam (J.W. de Bakker), and the Eindhoven University of Technology (W.P. de Roever), representing the areas of syntax, semantics and proof theory, respectively. The project is supported by the Netherlands National Facility for Informatics (NFI); its expected duration is four years starting in 1988. In the years 1984-1988, the same groups worked together in the Netherlands National Concurrency Project (LPC), supported by the Netherlands Foundation for the Advancement of Pure Research (ZWO). The research activities of the REX project include, more specifically: .1 Three subprojects devoted to the themes: • syntax of concurrent systems: a graph oriented framework for structures and processes • process theory and the semantics of parallel logic programming languages high-level specification and refinement of real-time distributed systems. • . Collaboration with visiting professors and post-doctoral researchers, in particular focused on the research themes mentioned above. In 1989/1990 these visitors include Dr. E.-R. Olderog (Kiel), Dr. W. Penczek (Warsaw), and Prof. P.S. Whiagarajan (Madras). . Workshops and Schools. In 1988 we organised a school/workshop on "Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency"; its proceedings appeared as Lecture Notes in Computer Science, Vol. 354, Springer, 1989. The workshop on "Stepwise Refinement of Distributed Systems" in 1989 is the second in a series of such events. For 1990, we plan a work shop on "Foundations of Object-oriented Languages" (FOOL). The educational activities of REX include regular "concurrency days". A concur- rency day may consist of tutorial introductions to selected topics, and of presentations of research results to a non-specialist audience. Often, experts from abroad are invited to contribute to these days. In addition, visiting professors are asked to present lec- ture series concerning recent developments in their fields of specialization. Clearly, the ~V school/workshops have the additional important function of providing their participants with an intensive introduction to new areas. Finally, we mention another aspect of the REX project. We are continuing the reg- ular contacts with other European projects in the area of concurrency built up during the LPC years. In particular, this applies to the French 3 - C Cooperation, Communi- cation, Concurrency - program, to the British Computer Society - the Formal Aspects of Computer Science group - and to groups within the Gesellschaft f/ir Mathematik und Datenverarbeitung (GMD) in Bonn. We would like to conclude this brief presentation of the future of the REX project by inviting everyone who is interested in more information concerning REX (possibility of visits, plans for workshops, other forms of exchanges, etc.) to write to one of the project leaders. J.W. de Bakker W.P. de Roever G. Rozenberg List of participants Ralph Back,/~bo Akademi Ron Koymans, T.U. Eindhoven Jaco de Bakker, C.W.I. Ruurd Kuiper, T.U. Eindhoven Howard Barringer, Manchester Bob Kurshan, AT&T Bell Labs. Univ. Simon Lain, Texas Univ. Frank de Boer, C.W.I. Leslie Lamport, Dig. Res. Center Ed Brinksma, Twente Univ. Kim Larsen, Aalborg Univ. Manfred Broy, Passan Univ. Nancy Lynch, M.I.T. Tineke de Bunje, Philips Res. Michael Merritt, AT&T Bell Labs. Labs. Jos Coenen, T.U. Eindhoven Carroll Morgan, Oxford Univ. Costas Courcoubetis, Crete Univ. Tobias Nipkow, Cambridge Univ. Werner Damm, Oldenburg Univ. Ernst-Rfidiger Olderog, Chr. At- Eduard Diepstraten, T.U. Eind- brecht Univ. hoven Paritosh Pandya, Tara .tsnI Hans-Dieter Ehrich, T.U. Braun- Amir Pnueli, "VVeizmann .tsnI schweig Lucia Pomello, Milan Univ. Hartmut Ehrig, T.U. Berlin Wblfgang Reisig, T.U. Munich Rob Gerth, T.U. Eindhoven Willem Paul de Roever, T.U. Rob van Glabbeek, C.W.I. Eindhoven Ursula Goltz, G.M.D. Marly Roncken, Philips Res. He Jifeng, Oxford Univ. Labs. Wim Hesselink, Groningen Univ. Grzegorz Rozenberg, Leiden Univ. Hendrik Jan Hoogeboom, Leiden Univ. Udaya Shankar, Maryland Univ. Jozef Hooman, T.U. Eindhoven Joseph Sifakis, IMAG Kees Huizing, T.U. Eindhoven Frank Stomp, Nijmegen Univ. Bernhard Josko, Oldenburg Univ. Jeannette Wing, C.M.U. Bengt Jonsson, Swed. Inst. CS Ping Zhou, T.U. Eindhoven Joost Kok, Utrecht Univ. Job Zwiers, Philips Res.Labs. Contents Preface • iii About the REX project ............................... v List of participants .................................. vii Invited lecture 1 M. Abadi, L. Lamport Composing Specifications ............................ 1 Technical Contributions 42 R.J.R. Back, J. noy Wright Refinement Calculus, Part h Sequential Nondeterministic Programs .... 42 R.J.R. Back Refinement Calculus, Part Ih Parallel and Reactive Programs ....... 67 .H Barringer, M. Fisher, .D ,yabbaG .G Gough, R. Owens METATEM: A Framework for Programming in Temporal Logic ...... 94 E. Brinksma Constraint-Oriented Specification in a Constructive Formal Description Technique .................................... 130 M. Broy Functional Specification of Time Sensitive Communicating Systems .... 153 .W Datum, .G DShmen, .V Gerstner, B. Josko Modular Verification of Petri Nets: The Temporal Logic Approach ..... 180 E. Diepstraten, R. I(uiper Abadi ~ Lamport and Stark: towards a Proof Theory for Stuttering, Dense Domains and Refinement Mappings ...................... 208 H.:D. Ehrich, A. Sernadas Algebraic Implementation of Objects over Objects .............. 239 R. van ,keebbalG .U Goltz Refinement of Actions in Causality Based Models .............. 267 M. Grofle-Rhode, .H Ehrig Transformation of Combined Data Type and Process Specifications Using Projection Algebras ............................... 301 He Jifeng Various Simulations and Refinements ..................... 340 B. Jonsson On Decomposing and Refining Specifications of Distributed Systems .... 361 B. Josko Verifying the Correctness of AADL Modules Using Model Checking .... 386 X J.N. Kok Specialization in Logic Programming: from Horn Clause Logic to Prolog and Concurrent Prolog ............................. 401 R.P. Kurshan Analysis of Discrete Event Coordination ................... 414 S.S. Lain,A .U. Shankar Refinement and Projection of Relational Specifications ........... 454 K.G. Larsen Compositional Theories Based on an Operational Semantics of Contexts 487 N.A. Lynch Multivalued Possibilities Mappings ...................... 519 .M Merritt Completeness Theorems for Automata .................... 544 .T Nipkow Formal Verification of Data Type Refinement -- Theory and Practice . . . 561 E.-R. goredlO From Trace Specifications to Process Terms ................. 592 P.K. Pandya Some Comments on the Assumption-Commitment Framework for Compositional Verification of Distributed Programs ............. 622 L. Pomello Refinement of Concurrent Systems Based on Local State Transformations . 641 A.U. Shankar, S.S. Lam Construction of Network Protocols by Stepwise Refinement ......... 669 F.A. Stomp A Derivation of a Broadcasting Protocol Using Sequentially Phased Reasoning .................................... 696 J.M. Wing Verifying Atomic Data Types ......................... 137 J. Zwiers Predicates, Predicate Transformers and Refinement ............. 759 R. Gerth Foundations of Compositional Program Refinement -- Safety Properties 777 Composing Specifications Martin Abadi Leslie Lamport Digital Equipment Corporation 130 Lytton Avenue Palo Alto, California 94301, USA Abstract A rigorous modular specification method requires a proof rule asserting that if each component behaves correctly in isolation, then it behaves correctly in concert with other components. Such a rule is subtle if a component need behave correctly only when its environment does, since each component is part of the others' environments. We examine the precise distinction between a system and its environment, and provide the requisite proof rule when modules are specified with safety and liveness properties.