**************************************************************************** The Third AMAST Workshop on Real-Time Systems; Models, Properties and Control Red Lion Hotel, Salt Lake City, Utah, USA March 6 - 8, 1996 This conference was sponsored by grants from the Office of Naval Research, Brigham Young University, University of Ottawa, and The University of Iowa. PROGRAM Wednesday, March 6-th Registration 8:30-9:00 Welcome: Conference Chair 9:00-12:30 Session 1: Modeling and verification, Chair: Zohar Manna 9:00--9:45 Nancy Linch (MIT), Modeling and verification of automated transit systems 9:45--10:00 Discussions and break 10:00--10:45 Steven P. Miller (Rockwell), Formal verification of avionics microprocessors 10:45--11:00 Discussions and break 11:00-11:30 D. Luis Llana, D.de Frutos, and M.Nunez, Testing semantics for urgent timed process algebra 11:30-12:00 T.Rus and H. Abu-Dagga, Synthesizing real-time programs from CoRE specifications 12:00-12:30 J. Alves-Foss, G. Saghi, and D. Frincke, Multilevel data security for real-time embedded computer systems: a case study 12:30-2:00 Lunch 2:00-5:30 Session 2: Simulation and verification, Chair: Nancy Linch 2:00-2:45 Zohar Manna (Stanford University), Verification of progress properties 2:45-3:00 Discussions and break 3:00-3:30 Muriel Jourdan, Integrating formal verification methods of quantitative real-time properties into a development environment for robot controllers 3:30-4:00 S. Kowalewski and J. Preussig, Analysis of time critical safety logic control for chemical processes 4:00-4:30 Coffee break 4:30-5:00 J. McManis, Verification of unpredictable real-time systems using suspension automata 5:00-5:30 J. Kosecka and H. Ben-Abdulah, An automated based algebra for specifying robotic agents Thursday, March 7-th Registration 9:00-12:30 Session 3: Design and validation, Chair: Steve Miller 9:00--9:45 Didier Begay (University of Bordeaux), Model-checking and protocol validation 9:45--10:00 Discussions and break 10:00--10:45 Jonathan Ostroff (York University), The design of real-time systems using standard untimed theories 10:45--11:00 Discussions and break 11:00-11:30 C. Lambiri and D. Ionescu, Real-time anddistributed models: composition, properties, and control 11:30-12:00 M. Bertran, F. Oller, F. Alvarez-Cuevas,A. Duran, and M. Porta, The Llul system (TLS). An integration of formalism and simulation for parallel-distributed and real-time software synthesis and development 12:00-12:30 M.Petriu, D.Petriu, and J.S.Basran, Modeling and verification of a multirobot assembly system 12:30-2:00 Lunch 2:00-5:30 Session 4: Logics and reasoning, Chair: Jonathan Ostroff 2:00-2:45 Scott Woodfield (BYU), Analysis of Real Time Systems Using OSA 2:45-3:00 Discussions and break 3:00-3:30 J.P.Katoen, D. Latella, E. Brinksma, and T. Bolognesi, A consistent causality based and interleaved view on a timed process algebra including timeouts 3:30-4:00 L. Urbina, A constraint logic programming for hybrid systems 4:00-4:30 Coffee break 4:30-5:00 P. Kosiuczenko and M. Wirsing, Timed rewriting logic 5:00-5:30 V. Yodaiken, Virtual logic analyzers and feedback: Moore machine models of real-time 7:30 Banquet Friday, March 8-th 8:00-12:00 Registration 8:30-12:30 Session 5: Temporal reasoning and model checking, Chair: Didier Begay 9:00--9:45 E. Allen Emerson (University of Texas as Austin), Quantitative temporal reasoning} 9:45--10:00 Discussions and break 10:00--10:45 George Milne (University of South Australia), The description and verification of a time sensitive protocol 10:45--11:00 Discussions and break 11:00-11:30 T.Rus and E. Van Wyk, Algebraic implementation of model checking algorithms 11:30-12:00 M. Faci and L. Logripo, An algebraic framework for the feature interaction problem 12:00-12:30 S. Yamane, The automatic verification system for real-time systems using symbolic model-checking 12:30 - 2:00 Lunch 2:00-5:30 Session 6: Process algebra and real-time systems, Chair: Dan Ionescu 2:00-2:30 F. Cuartero, D. de Frutos, and V. Valero, PCSP: a denotation model for probabilistic processes 2:30-3:00 F. Vazquez, Compositional model for formal development of real-time systems design 3:00-3:30 P. Bremond-Gregoire, H. Ben-Abdalah, and I. Lee, Ordering processes in a real-time process algebra 3:30-4:00 Concluding Remarks **************************************************************************** Registration The registration fee for this conference is $300. Payment must be made at conference registration desk using personal cheque, (international) money order, which must be in US dollars, or credit cards (VISA or Master Card). Cheques and money orders should be payable to "The University of Iowa". The registration fee covers lunch during the conference days, proceedings, banquet, and a trip to the Utah ski slopes. Reservations The Red Lion Hotel/Salt Lake City, is excited to be your host hotel for your March 6-8, 1996 Real-Time Programming Workshop. Currently, we have secured a block of over night guest rooms to be utilized by attending participants with arrival on Tuesday, March 5, 1996, and departure on Saturday, March 9, 1996. The special rate that has been established for this group is as follows: Single $ 109.00 Double $ 119.00 Triple $ 129.00 Quad $ 139.00 Please remember, it is important that you make your reservations early to receive the special rate established for this event. You can do this by calling the hotel's reservations department at (801) 328-2000. You can also use our 800 numbers 1-800-RED-LION or 1-800-547-8010. Please request the group rate for AMAST REAL-TIME PROGRAMMING Workshop to ensure that you are charged properly. Also, note that all reservation requests must be guaranteed by a first night room deposit or be guaranteed with a major credit card. Guest room reservations must be made in advance of February 14, 1996. Any individual reservations received after the cut-off date will be honored on a rate and space availability basis. The Red Lion Hotel/Salt Lake City provides 500 newly remodeled oversize guest rooms and is conveniently located in the heart of downtown Salt Lake City. We are only minutes from the Delta Center; home of the NBA Utah Jazz, the Triad Center, Capital Theater, Symphony Hall, the Crossroads Mall, and Utah's ski resorts, best known for the 'Greatest Snow on Earth' and other points of interest. The hotel also features such amenities as: free airport shuttle transportation, two restaurants, indoor heated pool, night club, hot tub, lobby lounge, health facilities, in-room coffee service. ****************************************************************************