\documentstyle [11pt]{article} \textwidth = 6.5in \textheight = 8.5in \topmargin = -0.3in \topskip = 0in \oddsidemargin = -0.1in \evensidemargin = -0.1in \addtolength{\parskip}{0.5ex} \begin{document} \begin{center} {\LARGE {\bf PROGRAM}}\\ \ \ \\ {\Large {\bf First AMAST International Workshop on Real-Time Systems}}\footnote {This conference is sponsored by grants from the National Science Foundation, Office of Naval Research, ESPRIT Basic Research Programme, University of Iowa, and University of Twente. }\\ {\Large {\it 1--3 November 1993, Iowa City, Iowa, USA}} \end{center} \medskip\noindent{\bf Organizing Committee:} \begin{quote} \begin{tabbing} Maurice Nivat, University of Paris VII, France\\ Charles Rattray, University of Stirling, Scotland\\ Teodor Rus, University of Iowa, Iowa City, IA, USA\\ Giuseppe Scollo, University of Twente, The Netherlands \\ \end{tabbing} \end{quote} \noindent {\bf Aim:} Dedicated real-time applications form one of the areas of great practical accomplishment of current computer technology. Real-time applications, however, bring to the fore new and intriguing questions regarding program specification, verification, and development. Correctness of solutions to the problems raised by real-time programming is particularly important due to the catastrophic nature of failure in real-time systems. This motivates the extensive work in the past decade on the formal theory of specification, verification, and development of real-time systems. At the same time, the AMAST movement, initiated in 1989 and aiming to use algebraic methodology for the development of software technology, has started to show practical results. The goal of this workshop is to expand the AMAST results to real-time system development, by: \begin{enumerate} \item Providing a forum for a dialog on the suitability of using algebraic methodology for real-time system development. \item Tracing the directions of a unifying approach for real-time system development within the framework provided by universal algebra. \item Promoting the integration of real-time system development within software technology based on the new algebraic methodology which is emerging from an AMAST approach. \end{enumerate} It is the intention of the organizers to publish the research reported at this workshop in a {\it Handbook on Real-Time System Development} in the AMAST Series in Computing. The feasibility of this project will be discussed in the special sessions scheduled during the workshop. We invite contributions to these discussions and submissions to the handbook from all attendees of the workshop. \medskip\noindent All meetings of this workshop will take %place in the room 345 (Northwestern) place at the Iowa Memorial Union. Each talk presented at this workshop will be 50 minutes long, followed by 10 minutes discussion. Supplementary discussion time will be provided in special sessions. \medskip\noindent Continental breakfast will be served each morning 8:30--9:00 at the meeting room. Lunch will be served each day 12:30--1:30 in BF 236, Second Floor, Iowa Memorial Union. \newpage {\small \noindent {\bf Monday, November 1-st, 9:00--12:30 Session 1} \medskip\noindent $\spadesuit$ 8:00--8:30 Registration and breakfast \medskip\noindent$\spadesuit$ 8:30-9:00 Opening address by Prof. David J. Skorton, Vice President for Research, The University of Iowa. \medskip\noindent 1. 9:00--10:00 {\it Finite Automata, Omega-Languages and Distributed Systems} by Maurice Nivat, Universit\'{e} Paris 7, France. \medskip\noindent 10:00--10:15 Coffee break \medskip\noindent 2. 10:15--11:15 {\it Issues in the Specification and Verification of Telephone Systems} by Luigi Logrippo, Department of Computer Science, University of Ottawa, Ottawa, Ont, Canada K1N 6N5. \medskip\noindent 11:15--11:30 Coffee break \medskip\noindent 3. 11:30--12:30 {\it On the Design of Timed Systems} by Juan Quemada, Departmento de Ingineria Telematica, Universidad Politechinica de Madrid, Spain. \medskip\noindent 12:30--1:30 Lunch break %\newpage \medskip\noindent {\bf Monday, November 1-st, 1:30--5:00 Session 2} \medskip\noindent 4. 1:30--2:30 {\it Visual Tools for Verifying Real-Time Systems} by Jonathan Ostroff, Department of Computer Science, York University, 4700 Keele Street, North York, Ontario, Canada, M3J 1P3. \medskip\noindent 2:30-2:45 Coffee break \medskip\noindent 5. 2:45--3:45 {\it Integrating State Machines, Temporal Logic, and Algebraic Models of Data} by Armen Gabrielian, UniView Systems, Mountain View, California, USA. \medskip\noindent 3:45-4:00 Coffee break \medskip\noindent 6. 4:00--5:00 {\it Towards Full Timed LOTOS} by Tommaso Bolognesi, C.N.R. Istituto CNUCE, 36, Via S. Maria, 56100 - Pisa, Italy. \medskip\noindent 5:00--8:00 Dinner \medskip\noindent$\bullet$ 8:00--10:00 Special session %\newpage \medskip\noindent {\bf Tuesday, November 2-nd, 9:00--12:30 Session 3} \medskip\noindent 7. 9:00--10:00 {\it Refining and Abstracting Time Information} by Steve Schneider, Oxford University, England. \medskip\noindent 10--10:15 Coffee break \medskip\noindent 8. 10:15--11:15 {\it Real-Time System = Discrete System + Clock Variables}, Part I by Rajeev Alur, AT\&T Bell Labs, Murray Hill, New Jersey, USA and Tom Henzinger, Department of Computer Science, Cornell University, Ithaca, New York, USA. \medskip\noindent 11:15--11:30 Coffee break \medskip\noindent 9. 11:30--12:30 {\it Real-Time System = Discrete System + Clock Variables}, Part II by Rajeev Alur, AT\&T Bell Labs, Murray Hill, New Jersey, USA and Tom Henzinger, Department of Computer Science, Cornell University, Ithaca, New York, USA. \medskip\noindent 12:30--1:30 Lunch %\newpage \medskip\noindent {\bf Tuesday, November 2-nd, 1:30--5:00 Session 4} \medskip\noindent 10. 1:30--2:30 {\it An Experience with the Formal Description in LOTOS and Prototyping of the Airbus A320 Flight Warning Computer} by Hubert Garavel, VERIMAG, Miniparc-ZIRST, rue Lavoisier, 38330 Montbonnot St Martin, France and Rene-Pierre Hautbois, Aerospatiale A/DL/EP, M 8621, 316 route de Bayonne, 31060 Toulouse cedex 03 France. \medskip\noindent 2:30--2:45 Coffee break \medskip\noindent 11. 2:45--3:45 {\it Specification and Proof in Real-time CSP} by Jim Davies, Department of Computer Science, University of Reading, Reading RG6 2AH, England. \medskip\noindent 3:45--4:00 Coffee break \medskip\noindent 12. 4:00--5:00 {\it The Priority Inversion Problem and Real-Time Symbolic Model Checking} by Edmund Clarke and Sergio V. Campos, Department of Computer Science, Carnegie Mellon University, Pittsburgh, PA, USA. \medskip\noindent 5:00--8:00 Dinner \medskip\noindent 8:00--10:00 Special Session %\newpage \medskip\noindent {\bf Wednesday, November 3-rd, 9:00--12:30 Session 5} \medskip\noindent 13. 9:00--10:00, {\it Using Synchronized Transition Systems to Develop Real-Time Software: An Experiment} by Didier Begay, Universit\'e Bordeaux I, LaBRI, 351, cours de la Lib\'eration 33405 Talence, France. \medskip\noindent 10:00--10:15 Coffee break \medskip\noindent 14. 10:15--11:15 {\it Verification of the Easylink Protocol} by Frits Vaandrager and Indra Polak, CWI and University of Amsterdam, The Netherlands. \medskip\noindent 11:15--11:30 Coffee break \medskip\noindent 15. 11:30--12:30 {\it Performance Analysis and True Concurrency Semantics} by Ed Brinksma, Joost-Pieter Katoen, Rom Langerak, and Diego Latella, Department of Computer Science, University of Twente, The Netherlands. \medskip\noindent 12:30--1:30 Lunch %\newpage \medskip\noindent {\bf Wednesday, November 3-rd, 1:30--5:00 Session 6} \medskip\noindent 16. 1:30-2:30 {\it Using Iterative Symbolic Approximation for Timing Verification} by David Dill and Howard Wong-Toi, Department of Computer Science, Stanford University, Stanford, CA, USA. \medskip\noindent 2:30--2:45 Coffee break \medskip\noindent 17. 2:45--3:45 {\it Analysis, Synthesis, and Optimization of Real-Time Systems in a Temporal Logic Framework} by Dan Ionescu, Department of Electrical Engineering, University of Ottawa, Ottawa, Ontario, Canada K1N 6N5. \medskip\noindent 3:45--5:00 Administrative matters and departure } \newpage \begin{center} {\Large {\bf General Information}} \end{center} \medskip\noindent All speakers at this workshop have been invited. Their presentations represent some of the best known research directions in real-time system development and we hope that their work will be of interest to a large audience. So, we would encourage all those who believe that they can benefit from these presentations to attend this workshop, to contribute to the discussions, and to further the development of real time systems. % by discussions during these three days of presentations. \medskip\noindent {\bf Location:} The conference will be held at the Conference Center of the University of Iowa\footnote{The University of Iowa does not discriminate in its educational programs and activities on the basis of race, national origin, color, sex, age, or disability. The University also affirms its commitment to providing equal opportunities and equal access to University facilities without reference to affectional preference. For additional information on nondiscrimination policies, contact the Coordinator of Title IX and Section 504 in the Office of Affirmative Action, telephone (319)335-0705, 202 Jessup Hall, The University of Iowa, Iowa City, Iowa 52242-1316. If you are a person with disability who requires reasonable accommodations in order to participate in this program, please contact the sponsoring department at (319)335-3231 to discuss your needs.}, Iowa Memorial Union. All meetings will be held in Room 345, Northwestern, at that location. \medskip \noindent {\bf Transportation} \begin{enumerate} \item The airport that services Iowa City is at Cedar Rapids, 25 miles from Iowa City. The closest international airport from Cedar Rapids is Chicago. Limousine services between Cedar Rapids airport and Iowa City are available. \item Interstate 80 is the easiest access route to Iowa City. Exit 244, Dubuque Street, leads you to downtown Iowa City. \end{enumerate} \noindent {\bf Climate:} It usually rains in Iowa City on November 1-st. However, considering the amount of rain we have had so far maybe it will be sunny this time. \medskip\noindent {\bf Registration fees}: \$150; this includes breakfast, lunch, coffee and refreshments, and the program and other documents distributed at the conference site. \medskip\noindent {\bf Hotel Reservation:} For hotel reservation please call 319-335-3513, Iowa House, indicating that you are attending the First AMAST International Workshop on Real-Time Systems. A block of rooms have been already reserved for you at \$52-single and \$58 double, a night. They will be assigned to the attendees on the basis of first come first served. The alternative is Holiday Inn -- downtown Iowa City -- which is within walking distance from the Iowa Memorial Union. The number to call is 319-337-4058, reservations. The Center for Conferences and Institutes is handling the registration and the other arrangements. For more information about reservation and registration contact: \begin{tabbing} Bobby C Davis or Lisa Barnes\\ Center for Conferences and Institutes \\ The University of Iowa, Iowa Memorial Union \\ Iowa City, Iowa 52242 \\ Phone (319)335-3220 \end{tabbing} \end{document}