Specification and Verification of Concurrent Systems

This volume contains papers presented at the BCS-FACS Workshop on Specification and Verification of Concurrent Systems held on 6-8 July 1988, at the University of Stirling, Scotland. Specification and verification techniques are playing an increasingly important role in the design and production of practical concurrent systems. The wider application of these techniques serves to identify difficult problems that require new approaches to their solution and further developments in specification and verification. The Workshop aimed to capture this interplay by providing a forum for the exchange of the experience of academic and industrial experts in the field. Presentations included: surveys, original research, practical experi ence with methods, tools and environments in the following or related areas: Object-oriented, process, data and logic based models and specifi cation methods for concurrent systems Verification of concurrent systems Tools and environments for the analysis of concurrent systems Applications of specification languages to practical concurrent system design and development. We should like to thank the invited speakers and all the authors of the papers whose work contributed to making the Workshop such a success. We were particularly pleased with the international response to our call for papers. Invited Speakers Pierre America Philips Research Laboratories University of Warwick Professor M. Joseph David Freestone British Telecom Organising Committee Charles Rattray Dr Muffy Thomas Dr Simon Jones Dr John Cooke Professor Ken Turner Derek Coleman Maurice Naftalin Dr Peter Scharbach vi Preface We would like to aeknowledge the finaneial eontribution made by SD-Sysems Designers pie, Camberley, Surrey.

Contenu

1. The Interplay of Theory and Practice in a Parallel Object-Oriented Language.- 2. Object-Oriented Process Specification.- 3. Formal Object Oriented Specification of Distributed Systems.- 4. The Design and Development of Ada Real-Time Embedded Systems.- 5. Protocol Analysis and Implementation using NPNs and SDL.- 6. A Tool for the Performance Analysis of Concurrent Systems.- 7. Winston: A Tool for Hierarchical Design and Simulation of Concurrent Systems.- 8. A Specification-Verification Framework for Distributed Applications Software.- 9. Dynamic Communication Links.- 10. Formal Environment and Tools Description for the Analysis of Real Time Concurrent Systems.- 11. An Equivalence Decision Problem in Systolic Array Verification.- 12. Should Concurrency be Specified?.- 13. Semantics for Specifying Real-Time Systems (extended abstract only).- 14. Specifying Processes in Terms of their Environments.- 15. Hennessy-Milner Logic with Recursion as a Specification Language, and a Refinement Calculus based on It.- 16. A Functional Programming Approach to the Specification and Verification of Concurrent Systems.- 17. Synchronization in Network Protocols.- 18. From Synchronous to Asynchronous Communication.- 19. Formal Specification and Verification of Asynchronous Processes in Higher-Order Logic.- 20. Temporal Specifications Directed by Grammar and Design of Process Networks.- 21. Analysis of Estelle Specifications.- 22. Concurrency in Modula-2: Properties of the Language Primitives.- 23. Specification and Implementation of Concurrent Systems using PARLOG.- 24. Specification and Verification in Communications Standards.- 25. Experience with LOTOS and Environment LOTTE on an ISDN Protocol.- 26. The Specification and Design of a Nondeterministic Data Structure Using CCS.- 27. A High-Level Petri Net Specification of the Cambridge Fast Ring M-Access Service.- Poster Sessions.- 1. Modelling of Distributed Problem Solving using Logic Modified Petri Nets.- 2. An Animator for CSP Implemented in HOPE.- 3. A Concurrent Approach to the Towers of Hanoi.- Author Index.