From ouimet@CA.UMontreal.IRO Mon Apr 10 15:11:57 1995 Received: from oxmail2.ox.ac.uk (oxmail2) by comlab.oxford.ac.uk id AA13054; Mon, 10 Apr 95 15:11:54 +0100 Received: from saguenay.IRO.UMontreal.CA by oxmail2.ox.ac.uk. with SMTP (PP) id <11798-0@oxmail2.ox.ac.uk.>; Mon, 10 Apr 1995 15:11:53 +0100 Received: from homard.IRO.UMontreal.CA (homard.IRO.UMontreal.CA [132.204.36.26]) by saguenay.IRO.UMontreal.CA (8.6.9/8.6.9) with ESMTP id KAA10162 for ; Mon, 10 Apr 1995 10:09:10 -0400 Received: (from ouimet@localhost) by homard.IRO.UMontreal.CA (8.6.9/8.6.9) id KAA09459 for Jonathan.Bowen@comlab.ox.ac.uk; Mon, 10 Apr 1995 10:09:07 -0400 Message-Id: <199504101409.KAA09459@homard.IRO.UMontreal.CA> From: ouimet@CA.UMontreal.IRO (Daniel Ouimet) Date: Mon, 10 Apr 1995 10:09:05 -0400 X-Mailer: Mail User's Shell (7.2.5 10/14/92) To: Jonathan.Bowen@comlab Subject: new call for papers Status: RO Hi, could you change in the www the call for papers for this new one: Thanks, Daniel ======================= There are 2 conferences announcement in this message: First is FORTE'95, and then at the end "Workshop on PROMELA/SPIN" which is held just before FORTE'95 in Montreal also. ============================================================================== Call for Papers FORTE'95 The 8th International IFIP Conference on FORMAL DESCRIPTION TECHNIQUES for Distributed Systems and Communications Protocols Montreal (Quebec), Canada, 17-20 October 1995 OBJECTIVE AND SCOPE FORTE'95 will address Formal Description Techniques (FDTs) applicable to Distributed Systems such as Estelle, Lotos, SDL, ASN.1, Z, Automata, Logics, Process, Algebras, etc., and will include industrial applicability to Protocols and Distributed Systems. The conference will be a forum for presentation of the state of the art in theory, application, tools and industrialization of (FDTs) and will provide an excellent orientation for newcomers. Research papers and industrial usage reports as well as proposals for tutorials (advanced technology seminars), poster displays and tool demonstrations are solicited. Topics of interests include (but are not restricted to) the following areas: - FDT-based software engineering - Design and implementation - Methodologies and architectures - Verification and validation - Comparative analyses of FDTs - Testing - Extensions of FDTs - Tools and tool support - Real-time and probability aspects - Practical experience and case studies - Examples and analyses of formal descriptions - Corporate strategic and financial consequences of FDT use. FORTE'95 will be sponsored by IFIP WG6.1. It will start with one day of tutorials and advanced technology seminars on 17 October 1995 and will continue with three days of technical presentations. Tool presentations and poster displays will be offered throughout all four days of FORTE'95. IMPORTANT DATES 30 April 1995 Submission deadline 15 July 1995 Notification of acceptance 30 August 1995 Camera ready copy for participants proceedings due CONFERENCE CO-CHAIRS G. v. Bochmann, R. Dssouli and O. Rafiq PROGRAM COMMITTEE P. Amer (Univ. of Delaware, USA), T. Bolognesi (CNUCE, Italy), J. Bowen (Univ. of Oxford, UK), E. Brinksma (Univ. of Twente, Netherlands), A. Cavalli (INT, France), S.T. Chanson (Univ. of Science and Technology, Hong Kong), J-P. Courtiat (LAAS, France), P. Dembinski (Academy of Science, Poland), J. deJMeer (GMD FOKUS, Germany), M. Ferguson (INRS, Canada), R. Gotzhein (Univ. of Kaiserslautern, Germany), M. Gouda (Univ. of Texas, Austin, USA), R. Groz (CNET, France), D. Hogrefe (Univ. of Bern, Switzerland), Y. Hirakawa (NTT, Japan), G. Holzmann (AT&T, USA), T. Kato (KDD, Japan), L. Kovacs (CAI, Hungaria), J. Kroon (PTT Research, Netherlands), G. Leduc (Univ. of Lige, Belgium), L. Logrippo (Univ. of Ottawa, Canada), G. Luo (BNR, Canada), L. Marshall (BNR, Canada), E. Najm (ENST, France), A. Obaid (UQAH, Canada), K. Parker (Telecom Research Lab., Australia), A. Petrenko (Univ. of Montreal, Canada), J. Quemada (Technical Univ. of Madrid, Spain), S. V. Raghavan (IIT, Madras, India), H. Rudin (IBM, Switzerland), K SUBMISSION POLICY Solicited are: Full original research papers and industrial usage reports, 5 copies, up to 16 pages (including bibliography), 12 point, single spaced, including an informative abstract as well as names and affiliations of all authors, and a list of keywords facilitating the assignment of papers to referees. A cover letter naming a contact author (including postal and email address) and indicating the preferred category (research paper or industrial usage report) in which the paper should be considered, is required. The cover letter should also state that the paper has not been presented in any language at another conference nor is it currently being considered by another conference or by a journal. Authors may propose a list of Program Committee members whom they consider to be particularly qualified to review their submission. Only those papers presented by an author during FORTE'95 will be included in the final proceedings which will be published by the official publisher of IFIP WG6.1. Proposals for tool demonstrations (including hardware and software requirements), poster displays, tutorials and advanced technology seminars. All submissions should be sent to: Prof. Rachida Dssouli Departement d'IRO Universite de Montreal Pavillon des sciences mathematiques et informatiques C.P. 6128 Succursale Centre-Ville (2920 Chemin de la Tour) Montreal, (Quebec) Canada H3C 3J7 Tel. : (514) 343 7599, Fax : (514) 343 5834 Email: dssouli@iro.umontreal.ca FOR FURTHER INFORMATION: Lucie Levesque Departement d'IRO Universite de Montreal Pavillon des sciences mathematiques et informatiques 2900, blvd Edouard-Montpetit (2920 Chemin de la Tour) Montreal, (Quebec) Canada H3T 1J4 Tel. : (514) 343 6111 (ext. 3520), Fax : (514) 343 5834 Email: forte95@iro.umontreal.ca ====================================================================== Workshop on PROMELA/SPIN (preliminary announcement) October 16th, Montreal, QC (just before FORTE'95) SPIN is a reachability analysis tool designed for the general verification of distributed systems. First made available publicly in 1991, a completely new version new version has recently been released. SPIN is used both for teaching and for industrial applications. It has inspired many other tools in various ways. This workshop aims at bringing together the community of users and researchers interested in SPIN as a tool, as well as an experimentation or a research vehicle. It will be an opportunity to discuss the current status of the tool, and the evolution of SPIN. We have identified the following areas of interest for this workshop: - bottlenecks in the practical application of verification technology and possible solutions that could be adopted in tools such as SPIN - effective methods for, and practical experience with, the modeling verification of large systems with SPIN - algorithmic improvements that should be considered - new types of verification - integration of SPIN with other tools, such as theorem provers, hardware design tools, code generators etc. - a panel on possible extensions of SPIN Further suggestions are most welcome. Participants are invited to present a position statement to be presented and discussed at the workshop. Workshop Organizer: INRS-Te'le'communications All Correspondance: gregoire@inrs-telecom.uquebec.ca -- Daniel Ouimet Pavillon Math-Info, bureau 2227 ouimet@iro.umontreal.ca Universite de Montreal, Dept. IRO. C.P. 6128, succursale Centre-Ville Montreal (Quebec) H3C 3J7, CANADA (514) 343-6111 ext. 3506 From lynnmar@ca.bnr Fri Jul 21 12:06:45 1995 Received: from oxmail.ox.ac.uk by comlab.oxford.ac.uk id AA04856; Fri, 21 Jul 95 12:06:38 +0100 Received: from x400gate.bnr.ca by oxmail.ox.ac.uk with SMTP (PP) id <03949-0@oxmail.ox.ac.uk>; Fri, 21 Jul 1995 12:02:16 +0100 X400-Received: by mta bnr.ca in /PRMD=BNR/ADMD=TELECOM.CANADA/C=CA/; Relayed; Fri, 21 Jul 1995 06:59:26 -0400 X400-Received: by /PRMD=BNR/ADMD=TELECOM.CANADA/C=CA/; Relayed; Fri, 21 Jul 1995 06:59:19 -0400 X400-Received: by /PRMD=BNR/ADMD=TELECOM.CANADA/C=CA/; Relayed; Fri, 21 Jul 1995 06:58:00 -0400 Date: Fri, 21 Jul 1995 06:58:00 -0400 X400-Originator: /dd.id=1643362/g=lynn/i=ls/s=marshall/@bnr.ca To: Pp-Warning: Parse error in original version of preceding line Original-To: :; X400-Mts-Identifier: [/PRMD=BNR/ADMD=TELECOM.CANADA/C=CA/;bcars735.b.747:21.06.95.10.59.19] X400-Content-Type: P2-1984 (2) Content-Identifier: FORTE'95 Prel... From: "lynn (l.s.) marshall" Sender: "lynn (l.s.) marshall" Message-Id: <"17754 Fri Jul 21 06:59:22 1995"@bnr.ca> Subject: FORTE'95 Preliminary Program X-Bulletin: FM People Status: R FORTE'95 PRELIMINARY PROGRAM 8th International Conference on FORMAL DESCRIPTION TECHNIQUES for Distributed Systems and Communications Protocols (FORTE'95) October 17 - 20, 1995 Montreal, Quebec, Canada Sponsored by IFIP WG 6.1 Organized by: Conference co-chairs Gregor v. Bochmann, Universite de Montreal and CRIM, Canada Rachida Dssouli, Universite de Montreal Omar Rafiq, Universite de Pau, France Local Arrangements, Registrations and Treasury Lucie Levesque, Universite de Montreal Coordination of tool demonstrations Daniel Ouimet, Universite de Montreal Program Committee: P. Amer (U. Delaware, USA), T. Bolognesi (CNUCE, Italy) J. Bowen (U. Oxford, UK), E. Brinksma (U. Twente, Netherlands) A. Cavalli (INT, France), S.T. Chanson (U. British Columbia, Canada) J.P. Courtiat (LAAS, France), P. Dembinski (Academy of Science, Poland) J. de Meer (GMD FOKUS, Germany), M. Ferguson (INRS, Canada) R. Gotzhein (U. Kaiserslautern, Germany), M. Gouda (U. Texas, Austin, USA) R. Groz (CNET, France), D. Hogrefe (U. Bern, Switzerland) Y. Hirakawa (NTT, Japan), G. Holzmann (AT&T, USA), T. Kato (KDD, Japan) L. Kovacs (CAI, Hungaria), J. Kroon (PTT Research, Netherlands) G. Leduc (U. Liege, Belgium), L. Logrippo (U. Ottawa, Canada) G. Luo (BNR, Canada), L. Marshall (BNR, Canada), E. Najm (ENST, France) A. Obaid (UQAH, Canada), K. Parker (Telecom Research Lab., Australia) A. Petrenko (U. Montreal, Canada), J. Quemada (Technical U. Madrid, Spain) S.V. Raghavan (IIT, Madras, India), H. Rudin (IBM, Switzerland) K. Saleh (Kuwait U., Kuwait), B. Sarikaya (U. Aizu, Japan) R. Tenney (U. Massachusetts, USA), K. Turner (U. Stirling, UK) S.T. Vuong (U. British Columbia, Canada) Financial Support from: INRS-Telecommunications Universite de Montreal Computer Research Institute of Montreal, (CRIM) Hewlett Packard-NSERC-CITI Industrial Research Chair on Communication Protocols Bell Canada TUTORIALS TUESDAY, October 17 Registration: 07h30 - 09h00 Room 1 Tutorial: (with midmorning coffee) 09h00 - 12h00 Symbolic Model Checking Edmund M. Clarke (School of Computer Science Carnegie Mellon University, USA) Logical errors in finite state reactive systems are an important problem for designers. They can delay getting a new product on the market or cause the failure of some critical device that is already in use. My research group has developed a verification method called {temporal logic model checking} for this class of systems. In this approach specifications are expressed in a propositional temporal logic, and reactive systems are modeled as state-transition graphs. An efficient search procedure is used to determine automatically if the specifications are satisfied by the state--transition graph. The technique has been used in the past to find subtle errors in a number of non-trivial circuit and protocol designs. During the last few years, the size of the reactive systems that can be verified by model checking techniques has increased dramatically. By representing sets of states and transition relations implicitly using Binary Decision Diagrams (BDDs), we are now able to check examples that are many orders of magnitude larger than was previously the case. In this tutorial we describe how the BDD-based model checking techniques work and illustrate their power by discussing the verification of several complex protocol and circuit designs. Lunch at the Hotel: 12:00 - 13:30 Tutorial: 13h30 - 16h30 Automatic Verification of Timed and Hybrid Systems Rajeev Alur (AT&T Bell Laboratories, USA) Traditionally, the focus of the research in formal methods has been qualitative temporal reasoning about behaviors of communicating processes. The decision to abstract away from quantitative time has had many advantages, but it is inadequate when reasoning about embedded systems that must interact with physical processes; the correct functioning of the control systems in devices from thermostats to airplanes depends crucially upon the continuous parameters. Consequently, in recent years there has been extensive research in developing methods for specification and verification of such embedded systems. This tutorial provides a selective sampling of modal logics and finite automata that admit automatic verification of real-time and hybrid systems. In the first part, we show how the model of transition systems can be augmented to model the behavior of real-time systems. Then we consider possible extensions of temporal logics to specify correctness requirements concerning timeliness. The model-checking problem is, then, to verify that a finite-state real-time system satisfies its specification given in timed temporal logic. We outline the basic algorithmic techniques needed to solve this problem, and survey the known complexity and decidability results. In the second part, we consider different heuristics to improve efficiency of the model-checking problem. In particular, we consider an iterative solution that incorporates the specified timing constraints in the model in an incremental fashion. This solution is implemented in the AT&T verifier COSPAN, and we discuss our experiences with the tool. The last part of the talk shows how the specification and verification methods generalize to hybrid systems systems comprising of a discrete program embedded in a continuously changing environment. Tutorial: 17h00 - 20h00 Formal Methods for the Synthesis of Discrete Event Systems A. Khoumsi and K. Saleh (University of Montreal, University of Kuwait, Kuwait) The aim of this tutorial is to present some formal and systematic methods for designing Discrete Event Systems (DES). DESs arise in the domain of computer networks and communication protocols, and also in other domains such as flexible manufacturing, robotics, process control. Two major approaches to the design of such systems are: Analysis and Synthesis. The latter is the main topic of this tutorial. Contrary to the analytic approach, the synthetic approach consists of proposing direct methods which do not require any further verification activities: the synthesized system is correct by construction. The tutorial is divided into three parts. The first part provides a survey and assessment of existing synthesis methods. The second part presents two relatively new synthesis methods. The first method has been developed for designing protocols for applications with temporal requirements. The second method has been developed for designing protocols using an approach inspired from the control theory of DESs. The third part proposes a more general and hybrid approach for designing DESs. It consists of combining the synthesis and analysis approaches for designing protocols. Room 2 Tutorial: (with midmorning coffee) 09h00 - 12h00 Formal design and implementation of high speed multimedia protocols Michel Diaz (LAAS du CNRS, France) The introductive part of the tutorial presents the general constraints that exist in distributed multimedia systems. Then the limits of the networks and the propoperties of the needed formal approaches will be given. The first section gives one formal basis for representing multimedia synchronisation in multimedia objects. This formal model allows one to represent flow based systems that include nominal, maximal and minimal durations, and that include temporal delays and jitters. A few basic models will be given based on Time Petri nets, leading to Time Stream Petri Nets (TSPN) and hierarchical TSPN. It will be shown how TSPN can be used for defining a general basic synchronisation inside multimedia objects. The second section of the tutorial will present a new solution for designing and implementing high speed multimedia protocols. Usual communication protocols are either connexion oriented or connectionless. It will be shown how these protocols, as UDP and TCP, are a specific case of a more general concept that will be presented, called a partial order connection. It is then explained how a partial order connection defines the more adequate transfer protocol for a specific multimedia information and how this connection is closely related to the formal TSPN model of the object. It will appear how the most adequate transfert protocol can be obtained, given a specific multimedia object, simply by deducing the partial order protocol from the partial order of the object synchronisation. Finally, the principle of implementing such a protocol will be given. Such an implementation is able to handle partial reliabilities and partial orders for a set of monomedia connections having different qualities of service. It will be shown how such implementations can provide the user with the best delay values and use of resources. Lunch at the hotel: 12:00 - 13:30 Tutorial: 13h30 - 16h30 High Performance Protocol Architecture Walid Dabbous (INRIA de Sophia Antipolis, France) The development of high speed networking applications requires efficient communication subsystems. In this tutorial, we will first give a rapid historical survey on protocols optimization techniques and on some high speed transport protocols developed for specific application needs. We will then show the need for a new protocol architecture based on the "Application Level Framing" (ALF) and "Integrated Layer Processing" (ILP) concepts. ALF states that applications send data as a sequence of autonomous "frames", which will be at the same time the unit of transmission, the unit of control and the unit of processing. This allows for efficient design of application specific protocols. It also enables ILP i.e. the integration of multiple transmission control layers in a single loop, maximizing the efficiency of modern processors. We will present both the architectural design aspects and the corresponding implementation problems. Practical experimentations with ALF and ILP will also be described and their benefits assessed. We will finally study how to automatically build communication subsystems for multimedia applications based on this architecture. Registration: 16h30-19h00 Cocktail: 17h00-19h00 CONFERENCE WEDNESDAY, October 18 Welcoming Remarks: 09h00 - 09h15 Invited Presentation: 09h15- 10h15 Specification and Verification of Timed Systems Joseph Sifakis (VERIMAG, France) We present a survey of recent results on the specification and verification of timed systems. Three different classes of formalisms are considered: Algebraic formalisms including operators that allow to express timing constraints like delays, timeouts, watchdogs. These formalisms can be considered as timed process algebras whose the most realistic representatives are the timed extensions of the Lotos language. Transition based formalisms which can be considered as extensions of automata or Petri nets with timing constraints. This class includes timed Petri nets and extensions of automata with continuous variables measuring the time elapsed such as timed automata and hybrid automata. Logical formalisms which are languages of the formulas of a logic with operators expressing timing constraints. Representatives of these formalisms are real-time temporal logics that are extensions of temporal logics with quantitative time and the Calculus of Durations. We show that as in the untimed case, all these formalisms admit a general common model: labeled transition systems with timed transitions. The existence of a common semantic framework allows a comparison of the classes. We focus on two particular problems: The translation of algebraic languages into transition based ones. This is a central problem for the compilation of algebraic timed languages into an executable model and it raises problems of compositionality, efficiency and optimality of the generated model. The verification by comparison of two transition-based descriptions or by comparison of a transition based description against a logical specification. We conclude by discussing issues concerning the applicability of the existing results and approaches and by pointing out some interesting research directions. Coffee break: 10h15 - 10h45 Session 1 Design Methodologies: 10h45-12h15 Distributed System Specification in VDM++, K. Lano (Imperial College, UK) OMT*, Bridging the Gap between Analysis and Design, K. Verschaeve, B. Wydaeghe, L. Cuypers, V. Jonckers, J. Heirbaut (VUB-INFO, Belgium) Formal Support for Design Techniques: A Timethreads-LOTOS Approach, D. Amyot, F. Bordeleau, R. J.A. Buhr, L. Logrippo (Univ. of Ottawa, Canada) Lunch-Demo at CRIM: 12h15 - 14h30 Buffet and tool demonstrations Session 2 Verification I: 14h30 - 15h55 Using Partial-Order Methods for the Verification of Behavioural Equivalences, M. Lara de Souza, R. de Simone (INRIA, France) Formal Verification of a Protocol for Communications over Faulty Channels, B. Chetali, P. Lescanne (CRIN-CNRS, France) Specifying Properties of Basic LOTOS Processes Using Temporal Logic, C. Kirkwood (Univ. of Glasgow, UK) A Reachability Analysis of RT-LOTOS Specifications, J.-P. Courtiat, R. C. de Oliveira (LAAS-CNRS, France) Coffee break: 15h55 - 16h15 Session 3 Algebraic Languages: 16h15 - 17h30 Towards a mobile LOTOS, E. Najm, J.-B. Stefani, A. Fe'vrier (ENST, CNET, France) Type Specifications with Processes, F. Puntigam (Technische Univ. Wien, Austria) A Unified Model for CSP-like Languages with Specifications, L. Lai (Univ. of Bradford, UK) THURSDAY, October 19 Session 4 System Specification and Z: 19h00 - 10h30 Secrets of Call Forwarding: A Specification Case Study, P. Zave (AT&T, USA) Formal Method for Event-triggered Sequential Systems, C. Petersohn (Christian- Albrechts Univ., Germany) An Extension of GDMO for Formalizing Managed Objects Behaviour, J. Keller (France Telecom, France) Coffee break: 10h30 - 11h00 Invited Presentation: 11h00- 12h00 Professor Mohamed Gouda (Univ. of Texas, USA) Lunch-Demo at CRIM: 12h15 - 14h30 Buffet and tool demonstrations Session 5 Industrial Experiences: 14h30 - 16h00 Experiences of using SDL collected in IskraTEL SDL Methodology, A. Robnik (IskraTEL, Slovenia) Development of Broadband ISDN Telecommunication Services using SDL'92, ASN.1 and Automatic Code Generation, U. Behnke, M. Geipl, G. Kurzbach, R. Mundstock, R. Schroder (Deutsche Telekom, Humboldt Univ. Germany) Supporting Evolution of SDL-based Systems: Industrial Experience, B. Gulla, J. Gorman (Norwegian Inst. of Tech. and SINTEF DELAB, Norway) Coffee break: 16:00 - 16h30 Session 6 Applying Formal Methods: 16h30 - 17h45 A LOTOS Compiler Generating Multi-threaded Object Codes, K. Yasumoto, T. Higashino, K. Abe, T. Matsuura and K. Taniguchi (Osaka Univ., Japan) A Comparison between the Service Addition Language SAL and the ITU-T Recommendation Z.120, S. Some, R. Dssouli, J. Vaucher (Univ. of Montreal, Canada) Combining Formal Methods: An Exercise in Integration, J.-Ch. Gregoire, M. Ferguson, L. Pino (INRS-Telecommunications, Canada) Formal Specification of a Framework for Synchronous Groupware Development, A. Kerbrat, S. Ben Atallah (Bull-IMAG, France) BANQUET : 19h30 FRIDAY, October 20 Session 7 Tools and Testing : 09h00 - 10h00 SELEXPERT - A Knowledge-based Tool for Test Case Selection, A. Guerrouat, H. Koenig, A. Ulrich (Otto von Guericke Univ., Germany, Brandenburg Univ., Germany, Hong Kong Univ., Hong Kong) Mutation Analysis Applied to Validate Specifications based on Petri Nets, S. Fabbri, J.C. Maldonado, P.C. Masiero, M.E. Delamaro, E. Wong (USP, Brasil, Bellcore, USA) A New Approach for Distributing Estelle Specifications, E. Lallet, S. Fischer, J.-F. Verdier (INT, france) Coffee break: 10h00 - 10h30 Panel - Formal Methods after 15 years: Status and Trends: 10h30 - 12h30 Lunch on your own: 12h30 - 14h00 Session 8 Real-time and Stochastic Systems: 14h00- 15h30 Critical Time Distributed Systems: Qualitative and Quantitative Analysis Based on Stochastic Timed Petri Nets, G. Juanole, L. Gallon (LAAS-CNRS, France) Testing Semantics for Probabilistic LOTOS, M. Nunez, D. de Frutos (Univ. Complutense de Madrid, Spain) Real-time LOTOS and Timed Observations, J. Davies, J. Bryans (Univ. of Reading, UK) Coffee break: 15h30 - 16h00 Session 9 Verification II: 16h00 - 17h30 Assertional Verification of a Connection Management Protocol, A. L. Olah, S. M. Heemstra de Groot (Univ. of Twente, Netherlands) Sharing Trees for "on-the-fly" Verification, F. Gagnon, J.-Ch. Gregoire, D. Zampunieris (INRS-Telecommunications, Canada, Facultes universitaires Notre-Dame-de-la-Paix, Belgique) Verification of Liveness Property for Communicating FSM's with Conditional Transitions depending on State Visiting Numbers, T. Higashino, A. Nakata, T. Itoh, K. Taniguchi (Osaka Univ., Japan) A New Approach for Protocols Performance Evaluation using Annotated Estelle Specifications, M. Hendaz, S. Budkowski (INT, France) TOOL DEMONSTRATIONS: Demonstrations of tools will be provided during the conference. They will be held on Wednesday and Thursday at CRIM (Centre de Recherche Informatique de Montreal) during a 2-hour lunch-demo (a little map will be provided). People interested in demonstrating tools are invited to contact Daniel Ouimet at Universite de Montreal (ouimet@iro.umontreal.ca). LOCATION Most of the events will be held at the Montreal Hilton Bonaventure Hotel, 1 Place Bonaventure, Montreal (Quebec), Canada, H5A 1E4 and the demonstrations will be held at CRIM, 1801, McGill College, office 800. CLIMATE The temperatures in late October range from the average high of 8!C to the 12!C. Rain showers are possible with, say, 30% probability. ATTRACTIONS The hotel is located in the heart of downtown Montreal, just minutes from commercial areas with plenty of animation and more rustic areas with Old World charm. Many visitors have enjoyed the numerous cafes, artists' hang-outs, boutiques and fine restaurants, and the district of Old Montreal against the backdrop of the St. Lawrence river. The organizing committee will provide special guidance to the better restaurants in the city. This period of the year is the time when the coulored leaves can be admired in the parcs of Montreal and throughout the forests in the area. TRANSPORTATION Air Canada has been appointed the Official Airline for FORTE'95. Call Air Canada at 1-800-361-7585 or your travel agent today and take advantage of: -Special convention rates for travel within North America, -Substantial savings with Air Canada and Continental Airlines' joint Convention fares, -Aeroplan or OnePass miles that can be redeemed on any Air Canada or Continental route, worldwide, -Savings up to 50% on the Regular Economy Class Fares, -Overseas passengers will be offered the best available fare. * Certain rules and conditions will apply. When purchasing your ticket, please ask that your Event Number: CV951464 be entered in the Tour Code box of your ticket, regardless of the fare purchased. Distance from Dorval Airport to the Montreal Hilton Bonaventure Hotel is less than 20 km. Distance from Mirabel International Airport to the Montreal Hilton Bonaventure Hotel is 60 km. The Dorval Airport shuttle to Montreal Hilton Bonaventure Hotel (costs 9,00$ CAN, and a taxi approximately 20$ CAN. The Mirabel Airport shuttle to central bus station costs 13,00$ CAN, and a taxi approximately 45$. The name of the shuttle company is Aeroplus (633-1100). Montreal Hilton Bonaventure Hotel is about 45 minutes driving from the Mirabel International Airport and 20 minutes from Dorval Airport, subject to good traffic conditions. ADVANCE REGISTRATION Please use a copy of this form to pre-register. Advance registration closes September 16, 1995. After this date, registration is subject to a late fee. Please mail your completed form with cheque (drawn on a North American Bank) or money order (in Canadian funds) or your Master card number (with your signature) payable to: FORTE'95 c/o Lucie Levesque Departement d'informatique et de recherche operationnelle Pavillon Andre Aisendstat Universite de Montreal 2900, blvd. Edouard-Montpetit (2219), Montreal, (Quebec), Canada, H3T 1J4 Tutorial registration fee covers: Attendance of tutorials, tutorial notes, lunch and coffee breaks on Tuesday, October 17. Conference registration fee covers: Conference admission, proceedings, reception on Tuesday night, lunches (except Friday), coffee breaks and the conference banquet dinner. Full and Student registrations fees cover: same as tutorial plus conference admission. Requests for refunds will be honoured until September 1, 1995. For further info. please contact Lucie at: (email): levesque@iro.umontreal.ca (phone) (514) 343-6111, extension 3520 or (fax) (514) 343-5834. FORTE'95 Registration Form Family name Given name Affiliation Address Postal code Country Phone number e-mail before Sept. 16 after Conference 550 600 Tutorial 300 350 Full 750 800 Student (1) 300 350 Additional banquet tickets 75 75 Extra proceedings 50 50 Total fee in canadian currencies ___________________ (1) Please attach proof of student status by ______ credit card (Master Card only) Name on credit card: _________________________ Credit card number: _________________________ Expiration date: _____________________________ Authorized signature: ________________________ Signing date: _______________________________ by ______ cheque drawn to a North American bank. by ______ money order in canadian currencies to FORTE'95 If you cancel, we must receive your cancellation by mail, fax or e-mail by September 1, 1995. HOTEL RESERVATION A block of rooms has been reserved for the FORTE'95 participants. Please mention that you are part of FORTE'95. Reservations* must be received by September 16, 1995. Reservations should be confirmed with either a check covering the first night's stay, or by any major credit card. The conference rate at the Hilton Bonaventure is $129.00 CAN (single or double occupancy). There is a charge of $25.00 per extra person up to a maximum of four (4)**. All rates are net, although the 7% goods and services tax (GST) is refundable to non-Canadian residents. Check-in time is 15h00 and check-out time is 12h00 noon. FORTE'95 Hotel Reservation Form Family name Given name Affiliation Address Postal code Country Phone number Arrival date/time __________________________ Single or double or Credit card Card No. Expiry date Signature ** If 3 persons share a room, it will cost 129$ + 25$ = 154$ divided by 3 persons = 52,00 $ per person per night ** If 4 persons share a room, it will cost 129$ + 50$ = 179$ divided by 4 persons = 44,75 $ per person per night * Please call, write or fax your reservation directly at the Montreal Hilton Bonaventure Hotel, 1, place Bonaventure, Montreal, Quebec Canada, H5A 1E4. International toll-free tel.: 1-800-445-8667 Tel.: 1-514-878-2332 Fax.: 1-514-3881 =========================================================================== From ouimet@CA.UMontreal.IRO Wed Aug 9 18:00:59 1995 Received: from oxmail.ox.ac.uk by comlab.oxford.ac.uk id AA11475; Wed, 9 Aug 95 18:00:54 +0100 Received: from saguenay.IRO.UMontreal.CA by oxmail.ox.ac.uk. with SMTP (PP) id <04369-0@oxmail.ox.ac.uk.>; Wed, 9 Aug 1995 17:59:34 +0100 Received: from homard.IRO.UMontreal.CA (homard.IRO.UMontreal.CA [132.204.36.26]) by saguenay.IRO.UMontreal.CA (8.6.12/8.6.12) with ESMTP id LAA00958; Wed, 9 Aug 1995 11:24:28 -0400 Received: (from ouimet@localhost) by homard.IRO.UMontreal.CA (8.6.12/8.6.12) id LAA17809; Wed, 9 Aug 1995 11:24:26 -0400 Message-Id: <199508091524.LAA17809@homard.IRO.UMontreal.CA> From: ouimet@CA.UMontreal.IRO (Daniel Ouimet) Date: Wed, 9 Aug 1995 11:24:25 -0400 X-Mailer: Mail User's Shell (7.2.5 10/14/92) To: forte95pc@CA.UMontreal.IRO, protodistlist@CA.UMontreal.IRO Subject: FORTE'95: Call for demo and poster Status: RO CALL FOR TOOL DEMONSTRATIONS AND POSTER DISPLAYS AT FORTE'95 The 8th International IFIP Conference on FORMAL DESCRIPTION TECHNIQUES for Distributed Systems and Communications Protocols Montreal (Quebec), Canada, 17-20 October 1995 OBJECTIVE AND SCOPE FORTE'95 will address Formal Description Techniques (FDTs) applicable to Distributed Systems such as Estelle, Lotos, SDL, ASN.1, Z, Automata, Logics, Process, Algebras, etc., and will include industrial applicability to Protocols and Distributed Systems. The conference will be a forum for presentation of the state of the art in theory, application, tools and industrialization of (FDTs) and will provide an excellent orientation for newcomers. Topics of interests include (but are not restricted to) the following areas: - FDT-based software engineering - Design and implementation - Methodologies and architectures - Verification and validation - Comparative analyses of FDTs - Testing - Extensions of FDTs - Tools and tool support - Real-time and probability aspects - Practical experience and case studies - Examples and analyses of formal descriptions - Corporate strategic and financial consequences of FDT use. Demonstrations of software tools and poster displays related to FORTE (FDT) will be provided during the conference. Proposals for demonstrations along with their hardware and software requirements and/or poster display, should be submitted before September 18, 1995. A number of SUN workstations running Unix will be available. Other kind of workstations could also be made available if there is enough request. After submission of your tool, you will be contacted for more informations and then a confirmation of the availability of hardware and software for your demo. Submit you tool demonstration or/and poster display to Daniel Ouimet. You will find a form to fill at the end of this message. e-mail: ouimet@iro.umontreal.ca Tel.: (514) 343-6111 ext. 3506 or leave message at (514) 343-6111 ext. 3520 Fax: (514) 343-5834 Address: Dept. IRO Universite de Montreal C.P. 6128 Succ. Centre-Ville Montreal, Qc CANADA H3C 3J7 _______________________________________ Please read the following form and fill it with your requirements. Also if you have any question, please redirect them to my e-mail. I will also ask you to send me a cartridge tape of your demo, so I can install it in advance on the machine (at least two weeks before) and try it before to be sure everything works fine. You can also send it with FTP if you prefer at an address I will provide later. ------------------------- SOFTWARE SHOULD BE RECEIVED AT THE LATEST ON OCTOBER 2, 1995. Machines will be configured as standalone workstations (not connected to network). Your software should already be compiled and linked (static library ONLY, no dynamic references since we could not assure you that we have the same library as you have), and ready to execute. If you need special compiler or interpreter, please include it with the tool. --------------------------- Form to be filled for tools --------------------------- Name of tool: Name of author: Address of author: (e-mail + fax + phone) Functions of the tool: Requirements of the tool Hardware type: Operating system: How much space needed on disk: How much swap space/real memory: Which interface it needs to operate: (Suntools) (OpenWindow) (X11R4) Does it need to be loaded at a special path, if yes which one(s): ================================================================ --------------------------- Form to be filled for poster displays --------------------------- Name of poster: Name of author: Address of author: (e-mail + fax + phone) Abtract of the poster (2-5 lines): Size of the poster display: ================================================================ -- Daniel Ouimet Pavillon Math-Info, bureau 2227 ouimet@iro.umontreal.ca Universite de Montreal, Dept. IRO. C.P. 6128, succursale Centre-Ville Montreal (Quebec) H3C 3J7, CANADA (514) 343-6111 ext. 3506