Formal Description Techniques, IV. Proceedings of the IFIP TC6/WG6.1 Fourth International Conference on Formal Description Techniques for Distributed Systems and Communications Protocols, FORTE '91, Sydney, Australia, 19–22 November 1991

✍ Scribed by K.R. Parker and G.A. Rose (Eds.)

• Publisher: North Holland
• Year: 1992
• Tongue: English
• Leaves: 580
• Category: Library

✦ Synopsis

Formality is becoming accepted as essential in the development of complex systems such as multi-layer communications protocols and distributed systems. Formality is mandatory for mathematical verification, a procedure being imposed on safety-critical system development. Standard documents are also becoming increasingly formalised in order to capture notions precisely and unambiguously. This FORTE '91 proceedings volume has focussed on the standardised languages SDL, Estelle and LOTOS while, as with earlier conferences, remaining open to other notations and techniques, thus encouraging the continuous evolution of formal techniques. This useful volume contains 29 submitted papers, three invited papers, four industry reports, and four tool reports organised to correspond with the conference sessions

✦ Table of Contents

Content:
IFIP Transactions C: Communication Systems, Page ii
Front Matter, Page iii
Copyright, Page iv
Preface, Page v, Ken Parker, Gordon Rose
Conference Chair, Page xi
Invited Speakers, Page xii
Sponsors and Cooperating Organizations, Page xiii
List of Authors, Page xiv
List of Referees, Page xv
Using LOTOS in a Design Environment, Pages 1-15, Mark Vigder, R.J.A. Buhr
Using VDM to Specify OSI Managed Objects, Pages 17-31, Linda Simon, Lynn S. Marshall
What is the Method in Formal Methods?, Pages 33-50, Ed Brinksma
Io: An Estelle Simulator for Performance Evaluation, Pages 51-66, D. Fernández, E. Vázquez, J. Vinyes
Modeling Timeouts and Unreliable Media with a Timed Probabilistic Calculus, Pages 67-82, Hans Hansson
Formal Methods at AT&T - An Industrial Usage Report, Pages 83-90, John A. Chaves
The Adoption of Formal Methods Within OTC, Pages 91-98, Karen Rosenberg
Linking Specifications with Implementations, Pages 99-108, Martin Kooij
Experience of Using LOTOS Within the CIM-OSA Project, Pages 109-116, Ashley M^c Clenaghan
An Exercise in Protocol Synthesis, Pages 117-131, Peter van Eijk, Jeroen Schot
Specification of a Distributed Coordination Function in LOTOS, Pages 133-148, Ing Widya, Franck Sadoun, Gert-Jan van der Heijden
XP, an experiment in modular specification, Pages 149-164, Gert Veltink
Understanding Interfaces, Pages 165-184, Simon S. Lam, A. Udaya Shankar
Modelling Dynamic Communication Structures in LOTOS, Pages 185-200, Lars-åke Fredlund, Fredrik Orava
Dynamic Configuration in LOTOS, Pages 201-216, Elie NAJM, Jean-Bernard STEFANI
An upward compatible timed extension to LOTOS, Pages 217-232, Guy Leduc
Mapping Time-Extended LOTOS To Standard LOTOS, Pages 233-248, Ashley M^c Clenaghan
LOTOS-like process algebras with urgent or timed interactions, Pages 249-264, T. Bolognesi, F. Lucidi
Event structures for design and transformation in LOTOS, Pages 265-280, Rom Langerak
A calculus to define correct transformations of LOTOS specifications, Pages 281-296, T. Massart
Inverse Expansion, Pages 297-312, S. Pavón, M. Hultström, J. Quemada, D. de Frutos, Y. Ortega
A LOTOS Data Facility Compiler (DAFY), Pages 313-327, Eric Lallemand, Guy Leduc
The superimposition of Estelle programs: A tool for the specification and implementation of observation and control algorithms, Pages 329-344, Benoît Caillaud
Design and Implementation of an Application Interface for LOTOS Processors, Pages 345-360, Kazuhito Ohmaki, Hirosato Tsuji, Kenjiroh Yamanaka, Yoshikazu Sato, Yoshinori Itabashi, Toshihiko Shimizu
Formal specification, validation and implementation of an Application protocol with Estelle, Pages 361-376, C.T. Nguyen, P. Hunel, M.-C. Vialatte
Specification and Validation of a Simple Overtaking Protocol using LOTOS, Pages 377-392, Patrik Ernberg, Lars-åke Fredlund, Bengt Jonsson
Protocol Trace Analysis based on Formal Specifications, Pages 393-408, M.C. Kim, Samuel T. Chanson, Son T. Vuong
Inheritance in LOTOS, Pages 409-424, Steve Rudkin
Mixing LOTOS and SDL Specifications, Pages 425-439, Heinz Saria, Heinrich Nirschl, Carl Binding
Λβ: a Virtual LOTOS Machine, Pages 441-456, José A. Mañas, Joaquín Salvachúa
Tool Demonstration: FORSEE, Pages 457-461, Jonathan Billington, Geoff Wheeler, Brian Keck, Ken Parker
Tool Demonstration: Tools for Process Algebras, Pages 463-466, Eric Madelaine, Didier Vergamini
Tool Demonstration: A Cross Compiling Experiment: a PC Implementation of a LOTOS Spec, Pages 467-470, José A. Mañas, Joaquín Salvachúa, Tomás de Miguel
Tool Demonstration: The Lotosphere Integrated Tool Environment Lite, Pages 471-474, Peter van Eijk
Superposition Refinement of Parallel Algorithms, Pages 475-493, R.J.R. Back, K. Sere
Specification and Verification of a Sliding Window Protocol in LOTOS, Pages 495-510, Eric Madelaine, Didier Vergamini
Protocol Verification System for SDL Specifications Based on Acyclic Expansion Algorithm and Temporal Logic, Pages 511-526, Hironori Saito, Toru Hasegawa, Yoshiaki Kakuda
Process Algebra Traces Augmented with Causal Relationships, Pages 527-541, C.J. Fidge
Fairness in LOTOS, Pages 543-558, Cheng Wu, Gregor v. Bochmann
A LOTOS Based Calculus with True Concurrency Semantics, Pages 559-574, Jean-Pierre Courtiat, Rosvelter João Coelho da Costa
IFIP, Pages 575-579