=============================================================================== PRELIMINARY CALL FOR PARTICIPATION AND ADVANCE PROGRAM ====================================================== Send queries to robert@cse.fau.edu The 1995 Workshop on Industrial-Strength Formal Specification Techniques WIFT'95 The Sheraton Inn, Boca Raton, Florida, USA April 5-8, 1995 Sponsored by the IEEE Computer Society, Technical Council on Software Engineering In cooperation with Florida Atlantic University WIFT'95 will bring together software engineering professionals from North America, Europe, and Asia to report on, analyze, and synthesize experiences related to the industrial applications of formal specification techniques. The workshop has three major parts: tutorials, general technical sessions, and working group sessions. The tutorials cover some of the more established formal methods tools, techniques and methods that are currently used in industries and government agencies. Papers in the general technical session vary from those that report on experiences, to those that present novel approaches to, and/or perspectives on, the industrial applications of formal methods. The group sessions provide highly-focused and structured forums for analyzing and synthesizing experiences related to the industrial uses of formal methods. There will also be a tools session in which demonstrations of tools supporting the building and manipulation of formal specifications will be given. (WWW users see http://www.cse.fau.edu/WIFT for information on WIFT'95) WIFT'95 Chairs -------------- Organizing Chairs: Robert France, Maria Larrondo-Petrie (Florida Atlantic University) Program Chair: Susan Gerhart (RICIS) Europe Coordinator: Tom Docker (CITI, England) Asia Coordinator: T. H. Tse (University of Hong Kong, Hong Kong) Tutorial Chairs: Betty Cheng (Michigan State University), Lesley Semmens (Leeds Metropolitan University) Technical Meeting Rates (US currency) ------------------------------------- Advance (until March 10) IEEE Members: $310 Non-members: $385 Full-time student IEEE members: $100 On-site (due after March 10) IEEE Members: $370 Non-members: $460 Full-time student IEEE members: $120 Tutorial Rates -------------- Advance - Half Day (until March 10) IEEE Members: $180 Non-members: $225 Advance - Full Day (until March 10) IEEE Members: $340 Non-members: $425 On-site - Half Day (due after March 10) IEEE Members: $215 Non-members: $270 On-site - Full Day (due after March 10) IEEE Members: $405 Non-members: $505 Registration Forms are available from: IEEE Computer Society, 1730 Massachusetts Ave. N.W., Washington, DC 20036-1992. tel: +1-202-371-1013; fax: +1-202-728-0884. WIFT Hotel Rate: $85 plus tax per night, single/double occupancy, until March 22, 1995 Call directly to make reservations at the Sheraton Inn, Boca Raton: Tel: +1-800-394-7829; Fax: +1-407-750-5437 PRELIMINARY WIFT'95 PROGRAM --------------------------- TUTORIALS Wednesday, April 5, 1995 (8am - 5pm) Morning Session (tutorials run in parallel) ------------------------------------------- ``Specification of Telephony systems with LOTOS'' Luigi Logrippo (University of Ottawa) ``Formal Development in B abstract machine notation'' K.Lano (Imperial College) H. Haughton (Imperial College) `` Rigorous Requirements for Real-Time Systems: Evolution and Application of the SCR Method'' S. Faulk (Kamen Sciences Corp.) C. Heitmeyer (U.S. Naval Research Laboratory) Afternoon Session (tutorials run in parallel) --------------------------------------------- ``Mechanically Checked Formal Specification and Verification using PVS'' John Rushby (SRI International) ``Z: An Active Approach'' Neville Dean (Anglia Polytechnic University) Michael G. Hinchey (University of Cambridge) ``The RSML notation and its application to TCAS II (Traffic alert and Collision Avoidance System II)'' M. Heimdahl (Michigan State University) TECHNICAL PROGRAM Thursday, April 6, 1995 (8am - 5pm) General Technical Session 1 - 9:am to 10:30am ------------------------------------------------------------- Formal Verification of the AAMP5 Microprocessor - A Case Study in the Industrial Use of Formal Methods Steven P. Miller, Collins Commercial Avionics, Rockwell International Corporation; Mandayam Srivas, SRI International, USA. The Architectural Specification of an Avionic Subsystem L. M. Barroca, Open University, J.S. Fitzgerald, U. Newcastle upon Tyne, L. Spencer, British Aerospace Defence Ltd.; UK Experiences in Applying Formal Methods to the Analysis of Software and System Requirements David Hamilton, Loral Systems; Rick Covington, John Kelly, Jet Propulsion Lab, USA. General Technical Session 2 - 10:45am to 12:15pm ------------------------------------------------- Inhibitors to Formal Method Exploitation - Cause or Symptom George Cleland , Donald MacKenzie, University of Edinburgh, UK. A C++ Library for Implementing Specifications C. Minkowitz, D. Rann, J. H. Turner, Staffordshire University, UK. Adding Formal Specifications to a Proven V & V Process for System-Critical Flight Software Jon Hagar, Martin Marietta Astronautics Company; James Bieman, Colorado State University, USA Group Sessions - 2pm to 5pm --------------------------- Group 1: Formal methods based processes co-chairs: Betty Cheng (Michigan State University) Tony Bryant (Leeds Metropolitan University) Group 2: Integrated formal and structured (including object-oriented) methods co-chairs: Pat Allen (Huddersfield University) Lesley Semmens (Leeds Metropolitan University) Group 3: Technology Transfer co-chairs: Susan Gerhart (RICIS) George Cleland (University of Edinburgh) Group 4: Formal methods in the development of real-time/critical/complex systems co-chairs: Mauro Pezze (Politecnico di Milano) Connie Heitmeyer (US Naval Research Lab) Tools session - 5:30pm - 8pm ------------------------------ Friday, April 7, 1995 (8am - 5pm) Guest Speaker: Pamela Zave (AT&T Bell Laboratories) - 8am to 9am General Technical Session 3 - 9:10am to 10:55am ----------------------------------------------- Automatic Verification of Industrial Designs V. Hartonas-Garmhausen, Union Switch and Signal, T. Jurfess, Georgia Institute of Technology, E. Clarke,, Carnegie Mellon University, D. Long, AT& T Bell Labs, USA. Timing Analysis of Industrial Real-Time Systems S. Campos, E. Clarke, W. Marrero, M. Minea, Carnegie Mellon University, USA. Automated Modular Specification and Verification of Real-Time Reactive Systems Jonathan S. Ostroff, York University, Canada. Formal Validation of Virtual Finite State Machines Alan R. Flora-Holmquist, Mark G. Staskauskas, AT& T Bell Laboratories, USA. General Technical Session 4 - 11am to 12:30pm --------------------------------------------- A Formal Approach to Reactive Systems Software: A Telecommunications Application in Esterel Lalita Jategaonkar Jagadeesan, AT& T Bell Laboratories, Carlos Puchol, U. Texas at Austin,, AT& T, USA. A Calculus of Hazard for Railway Signalling Michael Ingleby, David J. Mee, British Rail Research, UK. Experiences with Specification and Verification in LOTOS: A Report on Two Case Studies Carron Kirkwood , Muffy Thomas, U. of Glasgow, UK Group Session - 1:45pm to 5pm -------------------------- Groups 1, 2, 3, 4 continue to meet. Saturday, April 8, 1995 (8am - 12:30pm) --------------------------------------- 8am to 10am: Presentation of group sessions major results 10:10am to 12:15pm: PANEL: Promoting Formal Methods in Industry. This wrap-up panel will, among other things, comment on progress in the field as seen through WIFT'95 and identify further activities for promoting the industrialization of formal techniques.