infed@utrcu1 (infed) (05/10/89)
PROGRAMME Ninth International Symposium on Protocol Specification, Testing, and Verification 6th - 9th June 1989 Sponsored by IFIP WG 6.1 University of Twente, Enschede, The Netherlands --------------------------------------------------------- PROGRAMME COMMITTEE Ed Brinksma, Giuseppe Scollo, Chris Vissers : Programme Chair (Netherlands) Sudhir Aggarwal (USA) Gregor v. Bochmann (Canada) Tommaso Bolognesi (Italy) Andre Danthine (Belgium) Piotr Dembinski (Poland) Michal Diaz (France) Rudolf Jan Heijink Luigi Logrippo (Canada) (Netherlands) Bjorn Pehrson (Sweden) Rainer Prinoth (West Germany) Juan Quemada (Spain) Dave Rayner (UK) Harry Rudin (Switzerland) Krishan Sabnani (USA) Robin Sharp (Denmark) Deepinder Sidhu (USA) Norio Shiratori (Japan) Ken Turner (UK) OBJECTIVES The objective of the symposium is to bring together researchers and practitioners interested in the theory and application of formal techniques to the design, analysis, implementation and testing of opbn distributed systems. Being organized for the ninth consecutive year it is a well-established conference for all those who are active in this area of research, and at the same time provides an excellent orientation for newcomers. SYMPOSIUM THEMES The symposium ranges over the broad spectrum of topics that are related to the design, analysis, implementation and testing of open distributed systems. This year the following topics will be covered in particular: - formal specification of switching systems using Z, Estelle and LOTOS; - application of formal models: process algebras, transition systems, and temporal logic; - conformance testing: test generation, design and implementation of test systems; - compilation and transformation of formal description techniques; - tool environments; - verification by state space exploration. SYMPOSIUM FEATURES Attractive features of the symposium include: - a special tutorial day with three tutorial presentations by well-known specialists on important topics related to the Symposium's theme: the theory of distributed processes, on the development of software meta-tools (including demonstration), and on formal methods in conformance testing; attendants of the tutorial day will receive extensive tutorial notes for each of the presentations. - invited presentations by leading experts presenting the state-of-the-art of real-time design and verification, introducing the new research area of open distributed processing, and discussing the application and the industrialisation of formal methods. - the organization of small workshops on a number of 'hot' topics; these workshops are intended to stimulate the professional interaction among symposium participants. In addition to the invited presentations 26 refereed papers will be included in the symposium. The symposium proceedings will be published by North-Holland. Participants will receive a preliminary version of the proceedings; the first authors of accepted papers will receive the bound version. --------------------------------------------------------- TUESDAY, 6th JUNE 1989 TUTORIAL DAY 10.00-10.15 Welcome 10.15-12.00 Tutorial 1: ACP, an Algebraic Approach to Concurrency, ACP, the Algebra of Communicating Processes, is discussed as an algebraic framework for both specification and verification of communicating processes. A systematic algebraic approach is introduced to handle closely related languages and semantics, each of which may be optimized for different design and specification purposes. Verification is based on a simple compositional proof technique, using algebraic laws as well as 'trace logic'. speaker:Frits W. Vaandrager, CWI, Amsterdam Frits W. Vaandrager works since 1985 as a researcher in the theory of concurrency in the department of Software Technology at the Centre for Mathematics and Computer Science (CWI) where he participates in ESPRIT and RACE projects. 12.00-13.30 Lunch 13.30-15.15 Tutorial 2: The CENTAUR Meta-Tool System (includes tool demo), The tutorial discusses the design and organization of the CENTAUR meta tool system which produces - given the formal syntax and semantics - a language specific environment including a structure editor, an interpreter/debugger and other tools, all of which have graphic man-machine interfaces. Speakers: Gilles Kahn and Dominique Clement, INRIA/SEMA, Sophia Antipolis Gilles Kahn and Dominique Clement are with INRIA and the SEMA-Group and acted as project leaders in the development of the CENTAUR system. 15.15-15.45 Break 15.45-17.30 Tutorial 3: Formal Methods in Protocol Conformance Testing: from Theory to implementation (possible demo), The tutorial discusses the impact of a number of formal methodologies on the practical aspects of conformance testing, including testbed architecture implementation and automatic test script generation, and reporls on practical experience with the use of such tools in testing various protocol implementations. Speakers: Barry S. Bosik and M.Umit Uyar, AT&T Bell Laboratories, Holmdel Barry S. Bosik and M.Umit Uyar are with AT&T Bell Laboratories where they are resposible for the development of testing and verification theory, methodologies and tools and the practical applications thereof. 18.30-20.00 Welcoming Reception --------------------------------------------------------- WEDNESDAY, 7th JUNE 1989 08.50-09.00 Opening Prof. Dr. Ir. J.H.A. de Smit, Rector Magnificus University of Twente 09.00-10.30 Session 1: System Specification Chair: Juan Quemada, Politechnical University of Madrid *Signalling System No. 7, The Network Layer I.J. Hayes, University of Queensland, M. Mowbray, Overseas Telecommunications Commission, G.A. Rose, University of Queensland *Functional Specification for an ISDN Switching System: an Experience using Estelle M. Phalippou, CNET *Formal Specifications of Telephone Systems in LOTOS M. Faci, L. Logrippo and B. Stpien, University of Ottawa 10.30-11.00 Break 11.00-12.00 Invited Presentation: Design and verification of real-time distributed computing: an introduction to compositional methods Willem Paul de Roever and Jozef J.M. Hooman, Technical University Eindhoven 12.00-13.30 Lunch 13.30-15.00 Session 2: Process Algebra Applications Chair: Tommaso Bolognesi, CNUCE/CNR *A Verification Method for LOTOS Specifications and its Application N. Shiratori, H. Kaminaga, K. Takahashi, and S. Noguchi, Tohoku University *Stepwise Refinement of Layered Protocols by Formal Program Development T. Stroup, N. Goetz, Universitt Erlangen, and M. Mendler, University of Edinburgh *A Testing Theory for LOTOS using Deadlock Detection R. Langerak, University of Twente 15.00-15.30 Break 15.30-17.00 Session 3: Conformance Testing Chair: Rudolph Jan Heijink, PTT Research Neher Laboratories *Design and Implementation of a Ferry Clip Test System S.T. Chanson, B.P. Lee, N.J. Parakh, H.X. Zeng, University of British Columbia *On Test Sequence Generation for Protocols W.Y.L. Chan, S.T. Vuong and M.R. Ito, University of British Columbia *Protocol Conformance Testing Using Multiple UIO Sequences Y.-N. Shen, F. Lombardi, Texas A&M University, and A.T. Dahbura, AT&T Bell Laboratories. *The CO-OP Method for Compositional Derivation of Conformance Testers C.D. Wezeman, British Telecom 17.00-17.30 Break 17.30-19.00 Workshop 1: Approaches To Protocol Implementation Using Formal Methods Chair: Gregor von Bochmann, University of Montreal *Incremental Development of an HDLC Protocol in Esterel G. Berry, CMA-ENSMP + INRIA and G. Gonthier, AT&T Bell Laboratories *Distributed Implementation of LOTOS Multi-Rendezvous Qiang Gao and G. von Bochmann, University of Montreal *A Distributed Algorithm for Synchronous Process Communication at Ports P. Sjodin, SICS *Implementing Protocols with Multiple Specifications: Experiences with Estelle, LOTOS and SDL S.C. Murphy, Univ. of California, P. Gunningberg, SICS and J.P.J. Kelly, Univ. of California --------------------------------------------------------- THURSDAY, 8th JUNE 1989 09.00-10.30 Session 4: Specification Language Transformation Chair: Deepinder P. Sidhu, University of Maryland *A Multi-Processor Estelle to C Compiler to Experiment Distributed Algorithms on Parallel Machines C. Jard and J.M. Jezequel, IRISA *Combining ASN1 Support with the LOTOS Language G. von Bochmann and M. Deslauriers, University of Montreal *Compilation of LOTOS Data Type Specifications D. Wolz and P. Boehm, Technical University Berlin 10.30-11.00 Break 11.00-12.00 Invited Presentation: Open Distributed Processing, Joost J. van Griethuysen, Philips, Eindhoven 12.00-13.30 Lunch 13.30-15.00 Session 5: Transition System Applications Chair: Krishan K. Sabnani, AT&T Bell Laboratories *Verification and Formal Specification of ISO FTAM Using Numerical Petri Nets R. Lai, NEC Australia, T.S. Dillon, La Trobe University and K.P. Parker, CSIRO *Automated Verification of Equivalence of Protocol Machines *T. Higashino, Osaka University, K. Ninomiya, Daikin Industries, T. Kimoto, K. Taniguchi, Osaka University and M. Mori, Shiga University *Including a Queue in a Formal-Description-Driven Protocol Performance Analysis J. Gustafsson and H. Rudin, IBM Zurich Research Laboratory 15.00-15.30 Break 15.30-17.00 Session 6: Tool Environments Chair: Luigi Logrippo, University of Ottawa *On Executable Specifications, Validation, and Testing of MAC-Level Protocols P. Gburzynski and P. Rudnicki, University of Alberta *LOTOS Tools Based on the Cornell Synthesizer Generator P. van Eijk, University of Twente *A Semantics Based Verification Tool for Finite State Systems R. Cleaveland, University of Sussex, J. Parrow, SICS, and B. Steffen, University of Edinburgh *A Software Environment for OSI Protocol Testing Systems R.I. Chan, B.R. Smith, G. Neufeld, S.T. Chanson, S.T. Vuong, H.L. See, S. Chan, University of British Columbia and W.B. Davis, Idacom Electronics Ltd. 17.00-17.30 Break 17.30-18.30 Workshop 2: Graphics and Interactive Interfaces For FDTs Chair: Bjorn Pehrson, SICS *Generation of Graphic Language-Oriented Design Environments B. Backlund, P. Forslund, O. Hagsand and B. Pehrson *Adding Graphics to Estelle D. New and P.D. Amer, University of Delaware *Techniques for the Formal Definition of the G-LOTOS Syntax T. Bolognesi and D. Latella, CNR/CNUCE 20.00- Symposium Dinner Guest Speaker: H. Zimmermann, Chorus Systmes --------------------------------------------------------- Friday, 9th June 1989 09.00-10.30 Session 7: Verification by State Space Exploration Chair: Sudhir Aggarwal, Bellcore *Validating SDL Specifications: an Experiment G.J. Holzmann, AT&T Bell Laboratories *Dynamic State Exploration in Reachability Analysis M.-S. Chen, IBM T.J. Watson Research Centre and D.D. Dimitrijevic, Polytechnical University *Parallel Protocol Verification Using the Localized Approach: A Two-Phase Algorithm M.C. Yuang Bell Communications Research and A. Kershenbaum, Polytechnical University New York 10.30-11.00 Break 11.00-12.00 Invited Presentation: Formal methods: ambition versus reality, Jack P. Metthey, CEC, Brussels 12.00-13.30 Lunch 13.30-15.00 Session 8: Temporal Logic Applications Chair: Joachim Parrow, SICS *Verifying Safety and Deadlock Properties of Networks of Asynchronously Communicating Processes F. Orava, SICS *Extensions of Temporal Logic for Counting with Applications to Model Verification R.P. Kurshan, AT&T Bell Laboratories, S.S. Pinter, Yale University and B. Solomon, Technion Haifa *Axioms of Perfect Communication Using Temporal Logic with Past B. Pradin-Chezalviel and M. Diaz, LAAS du CNRS 15.00-15.10 Closing and Farewell --------------------------------------------------------- VENUE The symposium will take place at the University of Twente in The Netherlands. The university is situated between the cities of Enschede and Hengelo in the province of Overijssel in the eastern part of the country. The university campus (the only one in the country) is beautifully located in a park on the estate of Drienerlo, and offers ample sports and social facilities. The surrounding countryside is counted among the lost interesting landscapes of the country, and includes one of the few 'hilly' areas of The Netherlands. The participants will be accommodated in hotels in Enschede (pop. appr. 140.000). During the symposium transportation between the hotels and the campus will be provided at the beginning and end of each day; a regular bus service also connects the city centre with the campus (line 51, appr. 10 min., twice an hour). Hourly direct train services run between Enschede and all major Dutch cities and Amsterdam airport (Schiphol). Enschede is alsn linked to the country's extensive motorway system. Given the compact size of the country attending the symposium can be easily combined with a visit of the major Dutch historibal and cultural sights. REGISTRATION It is possible to register for: - the tutorial day (Tuesday, 6th June 1989); - the symposium proper (Wednesday to Friday, 7th-9th June 1989); - the tutorial day and the symposium. Registrations received after 1st May 1989 will be at a higher rate. Prospective attendants are advised to make their bookings as soon as possible in view of the high demand for accommodation in the month of June. The regular rates for the symposium include: - tea, coffee, refreshments and lunch on each day - the Symposium Dinner - transportation from and to hotels in the morning and at the end of each day's programme - a participant's version of the proceedings. The regular rates for the tutorial day include: - tea, coffee, refreshments and lunch - transportation from and to hotels in the morning and the evening - a participant's version of the tutorial notes. The reduced rates for students do not include lunches and the Symposium Dinner. For students cheap meals are available at the university's mensa (appr. fl.5 for a meal). To qualify for the reduced rates a proof of the student status should be mailed back with the application form. For registration and further information concerning the Symposium, please contact "ICSC Drienerburght", P.O. Box 217, 7500 AE Enschede, The Netherlands, phone: +31-53-893819 / 331366 fax : +31-53-356770 telex: 72378 icsc nl e-mail: hiddink@henut5.earn How to reach Enschede and the University of Twente By Air/Rail Fly to Amsterdam Airport (Schiphol). Trains for Enschede leave from the airport railway station regularly: - from 8.35 - 19.35 hrs. direct trains to Enschede leave every even hour at 35 minutes past the hour; - from 8.35 - 19.35 hrs. trains with destination Hengelo (with onward destinations in Germany) leave at every odd hour at 35 minutes past the hour, change at Hengelo station to connecting train to Enschede; - from 7.05 AM - 23.05 hrs. trains with destination Amersfoort (with onward destination Groningen / Leeuwarden) leave every hour at 5 minutes past the hour; change at Amersfoort station to connecting train to Enschede. The train trip takes two and a half hours. Those who wish to go to the University of Twente directly should leave the train at Hengelo station and take bus 51 to the university. By Car Coming from Amsterdam or Utrecht follow national highway A1 in the direction of Amersfoort, Apeldoorn, Deventer and then continue in the direction of Hengelo on the A35. Follow the signs for Enschede. For the University of Twente follow the signs marked 'Universiteit' at the end of the highway.