Subject: IEEE-CS TC-RTS Newsletter for Tue Sep 13, 1994 _______________________________________________________________________________ __ _ __ ___ ___ __ __ I E E E Technical Committee |\ | |_ | | (_' | |_ | | |_ |_) C S on Real-Time Systems | \| |__ |/\| ,_) |__ |__ | | |__ | \ _______________________________________________________________________________ Table of Contents Line ----------------- ---- 1. best@cs.bu.edu (Azer Bestavros) (549 lines) Announcement concerning the location of the IEEE-RTS Archives...... 3 Call for URLs ..................................................... 28 Report on the ACM SIGPLAN Workshop on LCTS for RT Systems.......... 52 2. Thomas Bihari (87 lines) Report from RTAW'94 for newsletters................................ 552 3. Frits.Vaandrager@cwi.nl (39 lines) CWI report available............................................... 639 4. Gerhard Fohler (55 lines) PhD thesis: Flexibility in Statically Scheduled Hard Real-Time Sy.. 678 5. krithi@iitm.iitm.ernet.in (Krithi Ramamritham) (410 lines) 15th IEEE Real-Time Systems Symposium: Advance Program............. 733 6. heitmeyer@nrl.itd.navy.mil (Connie Heitmeyer) (38 lines) Opportunity in Software Engineering R&D at Naval Research Lab...... 1143 7. NOSSDAV Workshop (116 lines) Workshop announcement.............................................. 1181 8. KBREWIN@apuk.co.uk (302 lines) New Journal - Real-Time Imaging.................................... 1297 9. ken@minster.york.ac.uk (26 lines) WWW page for the Real-Time Systems Research Group at York.......... 1599 10. "FORTE'94 Organization Committee" (897 lines) FORTE'94 - Completed Program / Registration Information............ 1625 ------------------------------------------------------------------------------ <<<<<<<<<<<<<<<<<<* START OF THE IEEE-CS TC-RTS NEWSLETTER *>>>>>>>>>>>>>>>>>> ------------------------------------------------------------------------------ Message 1; Postmarked Tue Sep 13 15:29:26 1994 From: best@cs.bu.edu (Azer Bestavros) Subject: Announcement concerning the location of the IEEE-RTS Archives Dear IEEE-CS TC-RTS list subscriber, Please note that the IEEE-RTS Archives have moved to a new machine. >From now on, please use the following machine for anonymous FTP requests: cs-ftp.bu.edu Also, please note that the WWW Home Page for the IEEE-CS TC-RTS has moved to the following URL: http://cs-www.bu.edu/pub/ieee-rts/Home.html Please update any pointers you may have (either to the FTP archives or to the WWW Home page) to reflect the abovementioned changes. If you maintain any pointers/links to the IEEE-RTS public archives (either to the FTP or WWW), please update your pointers/links. I apologize for any inconveniences these changes may cause. Subject: Call for URLs If your institution maintains publicly accessible archives explicitly for Real-time Research, you may want to have such archives linked to the IEEE-CS TC-RTS Home Page. To do so, please send me an email with the appropriate URL and I will link your institution up. As of 9/13/94, the real-time research groups at the following institutions are already linked to the IEEE-CS TC-RTS Home Page. 1. Boston University 2. University of Illinois at Urbana Champaign 3. University of Maryland 4. University of Massachusetts at Amherst 5. University of Michigan at Ann Arbor 6. University of Pittsburg 7. The Software Engineering Institute 8. University of Virginia 9. University of York --Azer Postmarked Fri Jul 12 16:15:14 1994 From: best@cs.bu.edu (Azer Bestavros) Subject: Report on the ACM SIGPLAN Workshop on LCTS for RT Systems ACM SIGPLAN Workshop on Language, Compiler, and Tool Support for Real-Time Systems June 21, 1994 Orlando, Florida (Summary of the workshop) Azer Bestavros Richard Gerber Steve Masticola (best@cs.bu.edu) (rich@cs.umd.edu) (masticol@scr.siemens.com) The first ACM SIGPLAN Workshop on Language, Compiler, and Tool Support for Real-Time Systems was held on June 21, 1994, in conjunction with the annual conference on Programming Language Design and Implementation. The workshop was well attended by researchers in both the programming language and real-time communities. The synergy between the two communities was remarkable and exciting; discussions were lively; and many attendees claimed that the workshop had stimulated new research ideas that they were going to pursue. The workshop was also notable for its level of discourse. Problems and ideas were traded freely, cleanly, and with almost a complete absence of confusing jargon. ``Novices'' and ``experts'' mingled freely; there was significantly more free-wheeling participation than one finds at established venues. For a first meeting, the turnout was also surprisingly international -- with papers from the UK, Germany, France, Canada and Austria. Based on this promising start, a second meeting of th Workshop will be held in 1995, in conjunction with the '95 PLDI conference in La Jolla, CA. This report summarizes the presentations given at the workshop. The summaries here have been rearranged to group similar topics together. For each of the papers described here, the presenter, rather than the full set of authors, is given. Topics, Themes and Controversial Questions ------------------------------------------ Bill Pugh and Tom Marlowe, in their roles as conference organizers, laid out the basic structure of the workshop and the topics they planned to cover. Then they asked Rich Gerber to posit a series of ``controversial questions, statements, and examples,'' with the intention of seeding the discourse for the remainder of the day. The issues raised by Pugh, Marlowe and Gerber included: (a) The difficulty of performing good timing analysis in the face of more complicated architectures (e.g., with hierarchical caches, multiple pipelines, shared and local memory, etc.). (b) The desire -- on the part of many managers and engineers -- to have complete traceability down to the machine-code level. (Reasons for this include inevitability of instruction-level debugging, etc.) (c) The implications of RISC architectures on embedded systems development, with respect to the compiler's effect on the code produced, its readability, etc. (d) The effect of generic compiler transformations in general: How the common reordering optimizations can inject errors in a real-time application by ``misinterpreting'' the programmer's intentions. (e) How compiler techniques can help programmers tune code (while preserving intended semantics), either automatically, or by simply identifying blocks that the programmer can move selectively -- perhaps with graphical tools. (f) How data-flow analysis techniques presented at PLDI conferences can be used in automated verification. (g) How Ada and Posix 1003.4-based systems can be used to support real-time systems. (h) That there are tremendous opportunities for programming language researchers in this domain, if they decide to pursue them. Gerber, a professor at the University of Maryland, sought to stimulate lively debate. His most memorable ``provocation'' was the proposition that the applicability of static, {\em a priori} timing analysis is exaggerated. His claim is that modern architectures are incredibly complicated; modeling pipelines, caches, shared memories, register windows, etc. using vendor-supplied benchmarks has become nearly impossible. This position provoked spirited discussion which continued throughout the day, both inside and outside the sessions. Gerber also observed that, when judging a system's performance, the end-to-end constraints are the only meaningful ones: examples are end-to-end response time, jitter, update rate and temporal correlation of input samples. He claimed that the periods of component processes -- which worry software researchers -- are just the artifacts used to achieve the original constraints. Since the intermediate deadlines are often selected by design engineers without careful thought, our efforts spent in meeting them are often wasted time. Gerber identified the major requirements for a real-time programming language: a source-level syntax for timing constraints, an unambiguous semantics which characterize the constraints, compiler technologies which preserve the semantics; and solid runtime support to carry out the programmer's intentions. Working Lunch ------------- After the morning session, the participants shared a working lunch, during which the ``compiler'' and the ``real time'' researchers were randomly distributed at the small tables. Some of the seed questions were informally pursued. For example, at one table David Chase (Thinking Machines) and Steve Tjiang (Synopsis) suggested how special RISC compilers could help alleviate the problems identified in (c)-(d) above. Keynote Tutorial: Ada '94 ------------------------- Ted Baker of Florida State University, who is working on the runtime system for the Gnu Ada project, gave a tutorial talk on the Ada '94 extensions for real-time support. Ada '94 includes extensions for object-oriented programming, numeric libraries, and real-time systems. In contrast to Ada '83, which is a single monolithic standard, Ada '94 includes a core language and extensions (including one for scheduling.) The legality of subsetting was emphasized in the new standard. Features for real-time support include: - Data sharing; both volatile and protected objects. - Asynchronous transfer of control: it overcomes many of the original problems with the synchronous ``rendezvous,'' it incorporates timeouts, and it has a clean semantics for exceptions. - DELAY UNTIL i.e., for absolute timing constraints. Questions about ``implementation'' and ``verification'' issues of code containing such a construct were raised. - Additional TIME types. - Entry service reordering via ``requeue'' statement. - Interrupt handling via ``protected procedures.'' - Priority-based scheduling, along with priority ceilings; and the ability to dynamically adjust priorities. - Low-level tasking primitives: SELECT THEN ABORT . This construct can support timeouts. Presentations on Language Design -------------------------------- Eric Rutten: SIGNAL ------------------- SIGNAL is a data flow language with notions of instantaneous reactions (clock, signal, etc.) Its target applications are reactive systems (signal processing, robotics). SIGNAL's approach is to define tasks and time intervals as primitive constructs. ``Signals'' are typed values indexed by time. ``Events'' are signals whose presence is the only important feature (i.e., clocks.) Equations are relations on data values and clocks. Carlos Pereira: C++/Real-Time UNIX ---------------------------------- Carlos Pereira (University of Stuttgart) gave a talk on a real-time C++ environment, built on top of the QNX Posix-compliant kernel. The goal of this language is the rapid prototyping of real-time systems, using standard C++ style templates. To maintain real-time control, Pereira has imposed a antisymmetric, ``communicates-with'' relation on object classes: Active classes map ``client instances'' to RT-UNIX processes, whereas interface objects define ``server instances'' to assist in interprocess communication. Paul Dasiewicz: Realtime programming in RTX--PARLOG --------------------------------------------------- In concurrent logic programming, there is typically no support for real-time programming. Dasiewicz addresses this in RTX--PARLOG. This support takes the form of abstract data types for ``time'' and ``duration,'' a scheduler with selective scheduling parameters (priority and task duration), and process timeouts. Garbage collection can be dynamically scheduled. RTX-PARLOG can generally produce only one solution to a program, since backtracking between processors is mostly eliminated due to guarded committed choice. Presentations on Timing Constraint Validation --------------------------------------------- Roderick Chapman: SPARK Ada formal methods ------------------------------------------ Roderick Chapman of the University of York (England) described SPARK Ada, a subset of Ada designed to be used in formal proofs of correctness of realtime systems. Chapman's proof system can not only prove the worst case execution time, but can also identify the program path which yields the worst case. Chapman divides the set of paths within a procedure into ``modes,'' one for each call site. This has interesting parallels with Landi aliasing and Pande def-use analysis; a mode would correspond, in abstract interpretation terms, to the (gamma) concretization of an assumed alias or assumed reaching definition. This work stems from an ongoing partnership between York and British Aerospace; it is a nice prototype for sound industrial/university collaborations. Alex Vrchoticky: Compilation Support for Execution Time Analysis ---------------------------------------------------------------- Compilation obscures the relationship between source and transformed code. Vrchoticky presented his timing tree data structure as a partial remedy to this problem. A timing tree is unchanged by local program transformations, and can in theory recover the timing assumptions of the original program. Presently this method cannot represent irreducible flow-graphs, or ``strong'' deviations between the source and generated code (e.g., those caused by loop unrolling.) Azer Bestavros: Toward Physically Correct Specifications -------------------------------------------------------- Azer Bestavros of Boston University spoke of a formal model and of a simulation/programming language (called ``Cleopatra'') for embedded control applications. The model/language prohibit users from specifying systems with certain physically-impossible features (e.g., lossless channels, exact delays, simultaneous dependencies, and constrained input transitions.) Bestavros argued that this ``ounce of prevention'' at the specification level is likely to spare a lot of time and energy in the development cycle -- not to mention the elimination of potential hazards that, otherwise, would go unnoticed. Plans for a Cleopatra-based programming environment to control robotics devices were mentioned. Kannan Narasimhan: Portable Execution Time Analysis --------------------------------------------------- Narasimhan described an extensible, pipeline-analysis tool for automated timing predictions. The tool uses a generic abstract architecture language to describe the CPU at hand, and can thus be applied to most RISC machines. Thus far the tool has been tested on the MPC601 (power PC), Sparc and R2000 processors. Presentations on Cache Modeling ------------------------------- Swagato Basumallick: Realtime Cache Survey ------------------------------------------ Swagato Basumallick of Iowa State reviewed several approaches for dealing with caches in realtime systems. (Caches are problematic for realtime computing, since they make it hard to predict the execution time of basic blocks.) The methods reviewed were: - Analysis by synthesis: Get the compiler to generate code whose behavior is easy to predict. - Graph coloring: Prove that cache lines are clear of interference. - Extended timing schema: Maintain state of cache information (must-hit, must-not-hit, may-hit) for each source statement. (See Mueller, below.) Basumallick advocated static scheduling to give a more global view of execution time requirements. However methods like static-priority dispatching could succeed, given {a priori} knowledge of the worst-case preemption overhead for every task pair. Frank Mueller: Predicting Instruction Cache Behavior ---------------------------------------------------- Frank Mueller of Florida State University described a tool to predict the behavior of instruction caches. Mueller uses a ``static cache simulator'' to determine which program lines are potentially cached. Program lines are divided into one of four categories on the basis of this analysis: Always Hit; Always miss; First Miss, then always hit; and Conflicts (miss sometimes, hit sometimes). Using this foundation, the instructions are annotated with a ``fetch from memory'' bit for schedulability analysis, etc. In a later talk (``Debugging Realtime Applications''), Mueller described the use of the static cache analyzer during dynamic testing. The idea is to instrument the program so that, in effect, it simulates its own cache behavior. Routines are linked in to provide hooks for a debugger to access the simulated cache state and execution time. This approach eliminates direct probe effect at the cost of a slowdown and some inaccuracy. Presentations on Architecture and Systems ----------------------------------------- Rajiv Gupta: Non-intrusive Monitoring ------------------------------------- Rajiv Gupta of the University of Pittsburgh presented a simple way to insert monitoring code into real-time computations. The idea is to find time periods that are necessarily idle. Instrumentation code is inserted within these periods. If it is not possible to instrument all the program points of interest at once, multiple runs are performed with different parts instrumented. This talk provoked significant debate. Some participants advocated using such methods as aggressively as possible, selectively creating (or widening) idle times in order to insert instrumentation code. Others disagreed, arguing that the ``temporary'' delay slots will effect the behavior of other processes in the system. These researchers suggested that once instrumentation code is placed in a module, it should remain there for good. Kevin Nilsen: Realtime Garbage Collection ----------------------------------------- Nilsen stressed the need to manage memory (via garbage collection or explicit allocation), and to control the time and space requirements of garbage collection. He described a hardware garbage collection memory manager (GCMM) device to redirect accesses to memory during garbage collection, while it is in the process of being moved. A major requirement of the hardware is that it not require special modifications to the processor. The GCMM supports a 1-2 microsecond latency time for allocate, deallocate, and access of memory, and has an average throughput 5 times higher than programs with explicit memory allocation (malloc). Mohamed Younis: Speculative Execution ------------------------------------- Timeliness via speculation has been used in hardware design (fast adders) and in real-time databases (speculative concurrency control). Younis argued that, in general, speculative execution can be used to speed up programs, but only where retraction of a speculatively executed code block would not cause a missed deadline. Source transformations may expose opportunities for speculative execution. Wrapup ------ Following the technical presentations, a set of short ``wrapup'' talks were given by Rich Gerber, Rajiv Gupta, Vivek Nirke, Alex Vrchoticky, and Mohamed Younis. Their objective was to identify to how programming languages and compiler techniques can help ease the real-time design and implementation process. Major points are are included in the following section. What came out of all of this? ----------------------------- It was generally agreed that several new areas should be pursued, and can be translated into hard results. They are: A. Languages and System Support: ------------------------------- - Languages for multimedia, generics for graphics, etc. are taken very seriously by the industrial real-time community, but are relatively neglected by researchers. Yet in many ways the problems are more challenging than those in hard real-time, and they require sound programming language support and tools. - Statistical real-time constraints: Most control systems over-sample to conservatively maintain the real-time constraints. Radical over-sampling doesn't scale up to support large systems, nor is it desired in multi-media systems. Constraints should allow for statistical ``softness'' in sampling and update jitter. Requirements languages should be capable of incorporating such constraints; programming languages to support these; and flexible runtime systems to run the applications. Also, automated tools would be useful to analyze and prototype such application. - There has been a proliferation of industrial real-time kernels, which are well-supported, lightweight, and incorporate sound real-time principles. To name three, QNX, VxWorks and LynxOS all support very low IPC latencies (around 10 microseconds), programmable timer-interrupt response within the same range, and priority-based scheduling. This being the case, there seems to be little further justification for universities or research labs to be in the realtime kernel-building business. Instead we can focus our efforts on what we do best: new design technologies, experimental applications, networks, etc., using off-the-shelf kernels and hardware platforms for our work. - Object-oriented programming is here to stay. C++ has emerged as the leading production language and Ada9x is incorporating many OO structuring paradigms. This being the case, we shouldn't overlook these technologies in real-time systems. The challenges lie in supporting dynamic binding, garbage collection, etc. B. Timing analysis: ------------------ - This is becoming a harder problem, but some vendors (like Sun) are modifying their architectures to accommodate real-time concerns. For example, the unpredictability inherent in Jump-and-link has led to a modification to the register windowing. (In future architectures, register spills will not trap to the kernel.) This change was made primarily for real-time applications, since Solaris is being marketed to them. - Nonetheless, tight bounds on timing estimates are getting harder to achieve. Compiler techniques can help in two ways: 1. By transforming the code to achieve better worst-case performance, accounting for caches, pipelines, etc. 2. By helping obtain better coverage in profiling samples; i.e., by lowering the variance between different execution time readings on similar traces. - No ``pure'' approach will suffice in timing analysis. In the design phase, we have to develop better statistical methods -- or perhaps better learn how to use the ones we have, e.g., Markovian models, simulation, etc. When the code is written, static analysis can be used as a first pass -- with certain refinements for caches, pipelines, etc. But nothing beats measuring a program's time on its (perhaps emulated) platform. For this we need better profiling/monitoring techniques, and superior ways of achieving reasonable coverage. C. Program Transformation Techniques: ------------------------------------ - Partial evaluation (and abstract interpretation) can produce better code, and is amenable to programs where variable definitions can be determined before schedule-time. - Transformations such as loop-invariant code motion can radically improve real-time programs, especially in obtaining schedulability. But code cannot be optimized for average case behavior; instead worst-case behaviors should be targeted. Thus generic back ends cannot be used, and should be customized for real-time applications. (The PLDI compiler folks had constructive ideas to accomplish this.) However, it was agreed that transformation techniques should not be carried out without the programmer's knowledge; instead, programmers should selectively apply them (perhaps using a graphical front-end). This would maintain traceability. D. Tools for Design Methodology: ------------------------------- - It was generally agreed that this is perhaps the most important problem. Topics addressed were appropriate models and logics, analysis techniques, and means of achieving design refinement. - A big problem is ``tuning'' the system's processes to achieve the end-to-end constraints. Compiler techniques can help here, by selectively 'cloning' shared servers and eliminating dead code. - Any system is destined to fail it is poorly designed, or if its design is incorrectly translated into an implementation. Thus a significant challenge is design refinement for mission-critical systems: Checking high-level, functional specs (perhaps via theorem provers or methods like Pugh's Omega Test); refining the spec into a more concrete system spec; checking its consistency via simulation, model-checking, etc.; developing the code with the aid of the abovementioned tools, so that it conforms to the system specs; tuning it via compiler-assisted transformation tools; and building clean and lightweight runtime systems to interact with the kernel intrinsics. This community seems to have a handle on many of these issues, and it may produce solid research toward the eventual goal. - It was generally agreed that fully automatic technologies will not suffice to solve these problems. The key is to find the right paradigms for user interaction. Future of the Workshop ---------------------- The strong consensus was that SIGPLAN should continue the workshop next year; in fact, when Tom Marlowe called for volunteers for the organizing committee, several participants quickly stepped forward. Many of the ``pure'' industrial compiler folks expressed interest in submitting papers and participating on panels. Industrial kernel people might profitably be recruited to attend, especially folks from QNX, Wind River, OSF and SUN (which is trying to put real-time functionality into Solaris). Finally, it is imperative to include several applications builders (i.e., ``customers''), especially in control systems and interactive graphics. For More Information -------------------- Postscript copies of some papers in the proceedings are available via anonymous FTP: ftp.cs.umd.edu:/pub/faculty/pugh/sigplan_realtime_workshop_94 or via the World-Wide Web http://www.cs.umd.edu/~pugh/sigplan_realtime_workshop_94 ------------------------------------------------------------------------------ Message 2; Postmarked Thu Jul 14 05:31:20 1994 From: Thomas Bihari Subject: Report from RTAW'94 for newsletters Application of Real-Time Research Explored at Workshop Thomas E. Bihari, AMT Systems Engineering The application of real-time systems research to real-world problems was the principal topic of the 2nd IEEE Workshop on Real-Time Applications held in Washington D.C., on Thursday and Friday, July 21-22, 1994. Alexander Stoyenko of the New Jersey Institute of Technology served as General Chair, and Steve Howell of the Naval Surface Warfare Center, and Jiandong Huang and Prabha Gopinath of Honeywell, Inc. served as Program Chairs. The workshop was attended by over eighty-five participants from academia, government, and industry. Twenty-six papers were presented on topics such as formal models, resource management, databases, fault tolerance, and of course a good variety of applications. Thursday's keynote talk was presented by Steve Vestal of Honeywell Technology Center. Steve traced the evolution of complex real-time applications. Earlier systems consisted of federated hardware and software components. Individual functions were developed as separate line-replaceable units (LRUs) with minimal interaction, and overall system control was achieved by many, small, separate PID controllers. More recently, such systems have become more integrated, where different software subsystems share hardware, and complex, multi-variable controllers are common. This requires a better understanding and enforcement of interactions between functions. Thursday evening's panel discussion "Real-Time Systems: Research to Technology to Applications" was led by Robert Harrison of the Naval Surface Warfare Center. In a vigorous debate, the panel (Tom Bihari of AMT Systems Engineering, Mike Hinchey of U. of Cambridge, Phil Laplante of Fairleigh-Dickinson U., Tom Lawrence of USAF Rome Labs, Bhavani Thuraisingham of MITRE, as well as Bob Harrison), and audience members discussed the perceived gap between real- time systems research and the needs of the real-time system developers. Concerns included the difficulty of scaling research results on small problems up to large real-world applications, and the need to integrate real-time tools and techniques into the common tools and techniques used by developers. The need for more interaction among the various parties was mentioned repeatedly. In Friday's keynote talk, Connie Heitmeyer of the Naval Research Laboratory discussed the state of the art in the use of formal methods for the specification and verification of real-time systems. Connie briefly presented 12 case studies of the use of formal methods on real systems (11 of which were successful), and then discussed NRL's experiences on several others in depth. Her conclusions were that formal methods are still not robust enough for general use, but that they have a real payoff in certain applications. For example, it cost $40M to formally verify 2K lines of code at the Darlington nuclear facility (where a serious mistake was uncovered), but the cost of an accident would have been much higher. This year's workshop was sponsored by the IEEE Computer Society Technical Committee on Real-Time Systems, with support from Honeywell, Inc., the Office of Naval Research, the Naval Surface Warfare Center, and New Jersey Institute of Technology's Real-Time Computing Laboratory, Institute for Integrated Systems Research, and Graduate Students Association. Next year's workshop will be held in conjunction with the First IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'95), November 9-13, 1995, in Florida. Also held jointly with ICECCS'95 will be the 5th Complex Systems Engineering Synthesis and Assessment Technology Workshop and the 20th IFIP/IFAC Workshop on Real-Time Programming. The goal of ICECCS'95 is to bring together the various communities that work with complex computer systems: academic researchers, industrial and government system developers, commercial tool vendors, etc. The conference is among new IEEE Computer Society activities recommended by the Technical Segments Committee on Engineering of Complex Computer Systems. Interested parties may contact Alexander Stoyenko, ICECCS'95 Conference Chair, at 201-596-3366 or "alex@vulcan.njit.edu" for more information. ------------------------------------------------------------------------------ Message 3; Postmarked Thu Aug 18 10:30:05 1994 From: Frits.Vaandrager@cwi.nl Subject: CWI report available The following CWI report is now available by anonymous ftp from ftp.cwi.nl as the file /pub/CWIreports/AP/CS-R9445.ps.Z : Authors: Doeko Bosscher, Indra Polak and Frits Vaandrager Title: Verification of an Audio Control Protocol Status: Report CS-R9445, CWI, Amsterdam, July 1994. To appear in T. Rus and C. Rattray, editors, Theories and Experiences for Real-Time System Development, 1994 An extended abstract will appear in Proceedings Third International School and Symposium on Formal Techniques in Real Time and Fault Tolerant Systems (FTRTFT'94), Luebeck, Germany, September 1994, LNCS. Springer-Verlag, 1994. This paper received the ``Best paper of FTRTFT'94 award''. Abstract: We analyze a simple version of a protocol developed by Philips for the physical layer of an interface bus that connects the various devices of some stereo equipment (tuner, CD player,...). The protocol, which uses Manchester encoding, has to deal with a significant uncertainty in the timing of events, due to both hardware and software constraints. We present a formal specification of the protocol, and a proof of correctness for the case where the tolerance of the clocks used within the system is less than $\frac{1}{17}$. A counterexample shows that the protocol fails for tolerances greater than or equal to this value. The verification is carried out using a model of linear hybrid systems, which is similar to the phase transition system model of Manna and Pnueli, and the model of linear hybrid automata of Alur, Henzinger and Ho. The semantics of linear hybrid systems is defined via a translation to the timed I/O automata model of Lynch and Vaandrager. ------------------------------------------------------------------------------ Message 4; Postmarked Mon Aug 29 10:35:03 1994 From: Gerhard Fohler Subject: PhD thesis: Flexibility in Statically Scheduled Hard Real-Time Systems "Flexibility in Statically Scheduled Hard Real-Time Systems", by Gerhard Fohler is available by FTP from ftp.vmars.tuwien.ac.at in the directory /pub/thesis in the file fohler.ps.Z The abstract of the thesis is as follows: "Static scheduling has been shown to be appropriate for a variety of hard real-time systems, mainly due to the verifiable timing behavior of the system and the complex task models supported. Its application is, however, impeded in systems with changing operational modes and critical activities, that arrive infrequently with unknown occurrence times. This thesis presents an approach to overcome these shortcomings. It addresses static scheduling, illustrated by an algorithm serving as case study, and provides concepts to extend the scope of statically scheduled systems to deal with mode changes properly and to provide for efficient handling of dynamic activities. Mode changes are performed by switching from one periodically executing static schedule to another via a special schedule to prepare for the change. As all involved schedules are constructed statically, all actions executing the mode change do so deterministically: Given the current mode, time, and mode change request, the exact executions during the mode change and their completion time are known before run-time. Dynamic activities are incorporated into static schedules by making use of the unused resources and leeways in the schedule. We present mechanisms to effectively maintain information about the amount of dynamic activity that can be accommodated without impairing the feasible execution of statically scheduled tasks. Ontop of this service, aperiodic tasks can be handled in a very simple way. We furthermore present an on-line guarantee algorithm. A combined approach integrates both methods." ------------------------------------------------------------------------------ Message 5; Postmarked Mon Sep 5 23:13:01 1994 From: krithi@iitm.iitm.ernet.in (Krithi Ramamritham) Subject: 15th IEEE Real-Time Systems Symposium: Advance Program 15th IEEE Real-Time Systems Symposium ===================================== December 7-9, 1994 Condado Plaza Hotel San Juan, Puerto Rico Sponsored by the IEEE Computer Society TC on Real-Time Systems General Chair Farnam Jahanian, University of Michigan Program Chair Krithi Ramamritham, University of Massachusetts Treasurer Walter Heimerdinger, Honeywell Publicity Chair Wei Zhao, Texas A&M University Industrial Chair Prabha Gopinath, Honeywell Local Arrangements Sandra Ramos-Thuel, AT&T Registration Linda Buss RTS-TC Chair Jack Stankovic, University of Massachsetts Program Committee Members George Avrunin Azer Bestavros Alex Buchmann Alan Burns Flaviu Cristian Wolfgang Halang Jayant Haritsa Michelle Hugue Kane Kim Hermann Kopetz Christian Koza John Lehoczky Jay Lala Jane Liu Miroslaw Malek Al Mok Frank Olken Raj Rajkumar Parmesh Ramanathan Karsten Schwan Alan Shaw Chia Shen Kang Shin Lorenzo Strigini Jay Strosnider Morikazu Takegaki Hide Tokuda Satish Tripathi Frits Vaandrager Tetsuo Wasano Victor Yodaiken ============================================================================== The purpose of RTSS is to provide an annual forum for exchanging emerging principles and practices underlying real-time computing. As in recent years, this year also we continue to witness the increasing interest in the area because of the better appreciation for the need for formal and scientific solutions for the highly interrelated problems involved in developing systems that have demanding correctness, dependability and timeliness characteristics. Many of the ideas that were formulated in academia in the recent past are being deployed in mainstream applications. This has given a major impetus to the field in which we are seeing a substantial number of new researchers tackling the many challenging problems that remain. All of these, on a worldwide scale, have led to RTSS attracting a large international contingent, in the program committee, in terms of the submissions, as well as in the acceptance of papers. We hope to see this trend reflected in the attendance as well. The technical program reflects recent developments in architecture, communication, databases, operating systems, performance, programming languages scheduling, and formal approaches for real-time applications. It also reflects an increased emphasis on system and tool implementation, evidencing a maturation of the underlying principles. To encourage the dissemination of findings in experimental development work, we have continued the synopses sessions from the previous three years. The conference will be preceded by the Workshop on Composability of Fault- Resilient Real-Time Systems, to be held December 6, 1995. Topics for discussion include the basic issue of design for composability and lessons learned in developing complex computing systems. Advanced registration is encouraged, as attendance is limited to 50 active practitioners and researchers in the field. Contact Michelle Hugue (meesh@cs.umd.edu) for details. We hope that you will join us in what promises to be a stimulating and important symposium. ============================= Advance Program ================================ Wednesday, December 7 8:00--8:45am Registration and Continental Breakfast 8:45--9:00am Introduction and Remarks 9:00--10:30am Session 1: Scheduling and Resource Allocation I (Chair: Raj Rajkumar, SEI/CMU) * "Efficient Aperiodic Service under Earliest Deadline Scheduling" Marco Spuri and Girogio Buttazzo (Scuola Superiore S. Anna, Italy) * "Mechanisms for Enhancing the Flexibility and Utility of Hard Real-Time Systems" N. C. Audsley, R. I. Davis and A. Burns (University of York, U.K.) * "Algorithms for Scheduling Hard Aperiodic Tasks in Fixed-Priority Systems Using Slack Stealing" Sandra R. Thuel (AT&T Bell Laboratories) and John P. Lehoczky (Carnegie Mellon University) 10:30--11:00am Coffee Break 11:00--12:00pm Session 2: Databases and Resource Management (Chair: Sang Son, Univ of Virginia) * "Timeliness via Speculation for Real-Time Databases" Azer Bestavros and Spyridon Braoudakis (Boston University) * "Resource Management for Continuous Multimedia Database Applications" Jiandong Huang (Honeywell, Inc.) and Ding-Zhu Du (University of Minnesota) 12:00--1:30pm Lunch 1:30--3:00pm Session 3: Communications I (Chair: Chia Shen, MERL) * "Scaling and Performance of a Priority Packet Queue for Real-Time Applications" Dan Picker and Ronald D. Fellman (University of California, San Diego) * "A Priority Forwarding Router Chip for Real-Time Interconnection Networks" Kenji Toda, Kenji Nishida, Eiichi Takahashi and Yoshinori Yamaguchi (Electrotechnical Laboratory, Japan) * "Multiple Route Real-Time Channels in Packet-Switched Networks Kai Chiu Kwan and Parameswaran Ramanathan (University of Wisconsin, Madison) 3:00--3:30pm Coffee Break 3:30--5:00pm Session 4: Compilers (Chair: Doug Locke, Loral Federal Systems) * "Busy-Idle Profiles and Compact Task Graphs: Compile-Time Support for Interleaved and Overlapped Scheduling of Real-Time Tasks" Rajiv Gupta (University of Pittsburgh) and Madalene Spezialetti (Lehigh University) * "An Accurate Worst Case Timing Analysis for RISC Processors Sang-Soo Lim, Young Hyun Bae, Gyu Tae Jang, Byung-Do Rhee, Sang Lyul Min, (Seoul National University), Chang Yun Park (Chung-Ang University), Heonshik Shin, Kunsoo Park, and Chong Sang Kim (Seoul National University, S. Korea) * "Compiler Transformations for Speculative Execution in a Real-Time System" Mohamed Younis (NJIT), Tom J. Marlowe (Seton Hall University) and Alex D. Stoyenko (NJIT) 7:00--10:00pm Buffet Banquet Thursday, December 8 8:00-8:45am Continental Breakfast 8:45--10:15am Session 5: Formal Methods (Chair: Lui Sha, SEI/CMU) * "The Generalized Railroad Crossing: A Case Study in Formal Verification of Real-Time Systems" Constance Heitmeyer (Naval Research Laboratory) and Nancy Lynch (MIT) * "Modeling and Analysis of Real-Time Ada Tasking Programs" James C. Corbett (University of Hawaii at Manoa) * "Response-Time Bounds of Rule-Based Programs under Rule Priority Structure" Rwo-Hsi Wang and Aloysius K. Mok (University of Texas, Austin) 10:15--10:45am Coffee Break 10:45am--12:00noon Synopsis Session 6: Experimental Systems and Applications (Chair: Bhavani Thuraisingham, Mitre Corp.) * "A Solution to an Automotive Control System Benchmark" Hermann Kopetz (Technical University of Vienna, Austria) * "Applying RMA to Improve a High-Speed, Real-Time Data Acquisition System" David del Val and Angel Vina (Universidad Autonoma de Madrid, Spain) * "ARINC 659 Scheduling: Problem Definition" T. Carpenter, K. Driscoll, K. Hoyme and J. Carciofini (Honeywell) 12:00noon--1:30pm Lunch 1:30--3:00pm Session 7: Tools (Chair: Christian Koza, Alcatel Austria) * "Bounding Worst-Case Instruction Cache Performance" Robert D. Arnold, Frank Mueller, David B. Whalley (Florida State University), and Marion G. Harmon (Florida A&M University) * "Deterministic Upperbounds of the Worst-Case Execution Times of Cached Programs" Jyh-Charn Liu and Hung-Ju Lee (Texas A&M University) * "Guaranteeing End-to-End Timing Constraints by Calibrating Intermediate Processes Richard Gerber, Seongsoo Hong and Manas Saksena (University of Maryland) 3:00--3:30pm Coffee Break 3:30--5:00pm Session 8: Scheduling and Resource Allocation II (Chair: Michelle Hugue, Trident Systems, Inc.) * "Scheduling Adaptive Tasks in Real-Time Systems" Kai Wang (Hughes Aircraft Co.) and Tein-Hsiang Lin (State University of New York at Buffalo) * "Dynamic End-to-End Guarantees in Distributed Real-Time Systems" Marco Di Natale and John A. Stankovic (University of Massachusetts) * "On-Line Scheduling to Maximize Task Completions" Sanjoy Baruah (University of Vermont), Nitin Sharma and Jayant Haritsa (Indian Institute of Science, Bangalore, India) 7:00-8:00pm IEEE Real-Time TC Business Meeting Friday, December 9 8:00--8:45am Continental Breakfast 8:45--10:15am Session 9: Communications II (Chair: Satish Tripathi, Univ. of Maryland) * "Probabilistic Bounds on Message Delivery for the Totem Single-Ring Protocol" L. E. Moser and P. M. Melliar-Smith (Univ. of California, Santa Barbara) * "Real-Time Communication Services in a DQDB Network" Rosa L. R. Carmo, Francisco Vasques and Guy Juanole (LAAS du CNRS, France) * "Analysing Real-Time Communications: Controller Area Network (CAN)" K. W. Tindell, H. Hansson (University of Uppsala, Sweden) and A. J. Wellings (University of York, U.K.) 10:15--10:45am Coffee Break 10:45am--12:00noon Synopsis Session 10: Formal Approaches and Languages Chair: Tom Lawrence, Rome Labs * "Computing Quantitative Characteristics of Finite-State Real-Time Systems" S. Campos, E. Clarke, W. Marrero, M. Minea (Carnegie Mellon University) and H. Hiraishi (Kyoto Sangyo University, Japan) * "Verifying an Intelligent Structure Control System: A Case Study" Wael M. Elseaidy, Rance Cleaveland and John W. Baugh, Jr. (North Carolina State University) * "Flexible Real-time SQL Transactions" Paul J. Fortier, (Naval Undersea Warfare Center) Victor Fay Wolfe and J. J. Prichard (University of Rhode Island) 12:00noon--1:30pm Lunch 1:30--2:45pm Synopsis Session 11: Operating Systems and Communications (Chair: Jim Ready, Microtec Research Inc.) * "Supporting Real-Time Traffic on Ethernet" Tzi-cker Chiueh and Chitra Venkatramani (State Univ. of NY at Stony Brook) * "Modeling DSP Operating Systems for Multimedia Applications" Daniel I. Katcher, Kevin Kettler and Jay K. Strosnider (Carnegie Mellon University) * "Emulating Soft Real-Time Scheduling Using Traditional Operating System Schedulers" Brad Adelberg, Hector Garcia-Molina (Stanford University) and Ben Kao (Princeton University) ================= RTSS 1994 Conference Registration Form ===================== Mail to: Linda Buss RTSS '94 Registration Rt. 1 Box 187B Menomonie, WI 54751 Phone: (715) 235-0487 Fax: (715) 232-6244 Email: rtss@eecs.umich.edu Name: Affiliation: Address: Phone: Fax: Email: IEEE Membership No: Workshop Fees: Category Before Nov. 21 After Nov. 21 IEEE Members $75 $95 Non-Members $90 $110 (No student rates available.) Symposium Fees: Category Before Nov. 21 After Nov. 21 IEEE Members $290 $360 Non-Members $375 $460 Full-time Students $95 $120 Workshop Fee: $ Symposium Fee: $ Total Due: $ This year, registrations can also be done through email (rtss@eecs.umich.edu). Conference registration includes admission to conference, copy of proceedings, continental breakfasts, coffee breaks, and the welcoming banquet on Wednesday night. The workshop fees include continental breakfast, coffee breaks and a copy of the workshop proceedings. The student fee includes all the events of the symposium. To receive student rate, students are required to have advisor's name and signature at the time of registration. Advisor name: Signature: Written requests for refunds must be postmarked no later than November 21, 1994. Refunds are subject to a $50 processing fee. All no-show registrations will be billed in full. Registrations after 11/21/94 will be accepted on-site only. NOTE: To save on postage, receipts will be given out at the conference. Payment can be made by check, money order, or credit card. Please make checks or money orders payable, in US currency, to RTSS'94. Credit Card: [] VISA [] Mastercard [] AMERICAN EXPRESS Credit Card Number: Cardholder Name: Credit Card Expiration Date: Total Charges Authorized: Signature: ====================== RTSS'94 Hotel Reservation Form ======================== Deadline: November 17, 1994 Mail to: Condado Plaza Hotel Attn: Reservation Department 999 Ashford Ave. San Juan, Puerto Rico 00902 Phone: (800) 468-8588 or (809) 791-1000 Fax: (809) 253-0178 Please complete all the information (type or print), and mail directly to the hotel. If faxing or phoning reservation, please mention IEEE Real Time Systems Symposium. RTSS'94 rates for each room for single or double occupancy are $123, plus 9% sales and occupancy tax. Accommodation desired: [] Single $123 [] Double $123 Name: Phone: Address: Arrival Date: Departure Date: Share Room With: Check-in is after 3:00pm, check-out is 12:00noon. A block of rooms has been reserved until November 17, 1994. After this date, room reservations will be accepted on a space available basis. The above special rates will also apply at least three days prior to and three days after the meeting dates based on availability to those who wish to extend their visit. One night's deposit is required with each reservation. A valid major credit card guarantee is acceptable in lieu of a cash deposit. Please check form of payment [] VISA [] MASTERCARD [] AMERICAN EXPRESS [] DINERS CLUB [] DISCOVER [] Check/Money Order Credit Card Number: Cardholder Name: Credit Card Expiration Date: Total Charges Authorized: Signature: ============================ See you in San Juan! ============================= ------------------------------------------------------------------------------ Message 6; Postmarked Thu Aug 4 12:06:09 1994 From: heitmeyer@nrl.itd.navy.mil (Connie Heitmeyer) Subject: Opportunity in Software Engineering R&D at Naval Research Lab R&D in formal methods, real-time computing, and CASE tools supporting the specification and verification of system and software requirements. The job involves design, documentation, and implementation of prototype toolset based on formal methods and software engineering principles. The employee will work with the existing staff of the SCR (Software Cost Reduction) Requirements Toolset project in their research activities. The position is a permanent one. Qualifications: - MS in Computer Science required. Ph.D. and an emphasis on Software Engineering, Real-Time Computing, or Requirements Engineering preferred. - Programming skills in C++, prior use of Motif, and prior experience in user interface design are strong pluses. - U.S. citizenship required. The Naval Research Laboratory is the premier Navy research laboratory and conducts both basic and applied research in computer science (including real-time computing, software engineering, requirements specification and verification, mechanical verification, computer security, and formal methods) and artificial intelligence. Located in Washington, DC, the laboratory is an equal opportunity employer. Please send resume (e-mail preferred) to: Connie Heitmeyer Code 5546 Naval Research Laboratory Washington, DC 20375 e-mail: heitmeyer@nrl.itd.navy.mil fax: (202) 767-9197 ------------------------------------------------------------------------------ Message 7; Postmarked Mon Aug 22 11:33:23 1994 From: NOSSDAV Workshop Subject: Workshop announcement 5th International Workshop on Network and Operating System Support for Digital Audio and Video (NOSSDAV '95) CALL FOR PAPERS April 19, 20, 21, 1995 Durham, New Hampshire, USA Sponsored by the IEEE Communications Society In cooperation with ACM SIGCOMM, SIGOPS, SIGMM, SIGGRAPH, and SIGIR Network and operating system support for digital audio and video are becoming increasingly important with the convergence of the computer, the TV, and communications. Innovation in this field is fueling the industry developments in interactive multimedia services to the home. In the past, research in this domain has largely originated as adaptations of specific technologies to support audio and video. This work has lead to an understanding of common cross-disciplinary problems. Increasingly, this work encompasses and integrates the diverse technology necessary to achieve end-to-end systems. To this end, research leading to complete solutions is viewed as particularly important to the workshop. The workshop is intended to bring together practitioners from a variety of areas, including communications and networks, operating systems, real-time systems and distributed computing. It is intended that an outcome of the workshop will be a statement of the the state of the art in this field, highlighting the major areas requiring future research. Relevant topics for the workshop include: High-speed/ATM networks Multimedia-oriented desk, local, and wide area networks Workstation architectures for multimedia Cell-based system architectures Multimedia network interfaces Communication protocols for multimedia Multicast Micro-kernel and OS support for real-time communications Resource management and reservation in the OS and network End-to-end admission control Quality of service and synchronization frameworks Multimedia storage, server, and I/O architectures Distributed multimedia systems APIs and CM programming abstractions for multimedia Community networking TV set-top device communication Instructions for Submitting Papers: Two types of submissions are solicited: position papers and research papers. For the purpose of paper review, position papers are restricted to three single-spaced ASCII pages. Research papers are restricted to an extended abstract no longer than five formatted postscript pages. Papers should be electronically mailed to nossdav95@spiderman.bu.edu Only if electronic submission is impossible, papers may be sent to: Prof. T.D.C. Little, Multimedia Communications Laboratory, Department of Electrical, Computer and Systems Engineering, Boston University, 44 Cummington Street, Boston, MA 02215 USA. Tel: +1 617 353-9877 Fax: +1 617 353-6440 tdcl@bu.edu. The proceedings of the workshop will be published by Springer-Verlag and the best papers will be forwarded to selected journals for publication. Important Dates: Abstracts due: December 12, 1994 Acceptance notification: January 25, 1995 Final paper due: March 8, 1995 Workshop: April 19, 1995 Program Co-Chairs: Riccardo Gusella, HP Labs, USA T.D.C. Little, Boston University, USA Program Committee: Stavros Christodoulakis, Technical University of Crete Domenico Ferrari, University of California, Berkeley Ralf Herrtwich, IBM Creative Multimedia Studios Andy Hopper, Olivetti & University of Cambridge Kevin Jeffay, University of North Carolina at Chapel Hill Chuck Kalmanek, AT&T Bell Laboratories Jim Kurose, University of Massachusetts at Amherst Aurel Lazar, Columbia University Derek McAuley, Cambridge University Duane Northcutt, Sun Microsystems Laboratories Guru Parulkar, Washington University Steve Pink, Swedish Institute of Computer Science Radu Popescu-Zeletin, GMD-FOKUS K.K. Ramakrishnan, Digital Equipment Corporation P. Venkat Rangan, University of California, San Diego Jon Rosenberg, Bell Communications Research Eve Schooler, USC/Information Sciences Institute Doug Shepherd, Lancaster University Cormac Sreenan, AT&T Bell Laboratories Jean-Bernard Stefani, France Telecom/CNET Daniel Swinehart, Xerox PARC Hideyuki Tokuda, Carnegie Mellon University/Keio University Jon Walpole, Oregon Graduate Institute of Science & Technology Raj Yavatkar, University of Kentucky This CFP is on-line at http://spiderman.bu.edu. ------------------------------------------------------------------------------ Message 8; Postmarked Mon Jul 18 16:18:42 1994 From: KBREWIN@apuk.co.uk Subject: New Journal - Real-Time Imaging Academic Press are proud to announce the publication of a new journal - Real-Time Imaging. The first issue will be published in the Spring of 1995. I am enclosing a call for papers for the journal, and would be most grateful if you could post it on the the newsletter on real-time systems. Please do not hesitate to contact me if you would like nay further information. With best wishes Kate Brewin Editor kbrewin@apuk.co.uk CALL FOR PAPERS Aims and Scope Real-Time Imaging is a new multidisciplinary peer-reviewed technical journal that will serve as a convergence point for researchers, technologists and practitioners in fundamental real-time imaging technologies and their application areas. It is intended that this journal will be the first place that new fundamental and practical advances in real-time imaging are unveiled. Examples of areas to be covered include; o image compression o target acquisition and tracking o remote control and sensing o image enhancement and filtering o networking for real-time imaging o advanced computer architectures o computer vision o optical measurement and inspection o simulation These technologies are critical in such applications as o robotics o virtual reality o multimedia o medical imaging o industrial inspection o high-definition television o advanced simulators o computer-integrated manufacturing o intelligent vehicles The journal will focus on papers of an applied nature although survey and theoretical papers with practical results are welcome. In order to maintain the central focus of the journal and to encourage a cross-disciplinary emphasis, the journal solicits papers that involve systems or technologies that are relevant in at least two of the stated applications areas. All submissions will be rigorously peer-reviewed. Audience Real-Time Imaging is aimed at industrial, academic and government scientists and practitioners who are researching and developing real-time imaging technologies and applications. The journal provides a mechanism for researchers to keep abreast of new applications and industrial needs, and for practitioners to learn of new available technologies. Editors-in-Chief Phillip A. Laplante, Fairleigh Dickinson University, Madison, New Jersey, 07490 USA. Alexander D. Stoyenko, New Jersey Institute of Technology, Newark, New Jersey, 07102 USA Editorial board An international group of board members has been appointed to represent major disciplines, and manage the rapid review of papers. David P. Casasent, Ctr. for Excellence in Optical Data Processing, Carnegie Mellon University, USA E.R. Davies, Department of Physics, Royal Holloway, University of London, Surrey UK (European Co-ordinator) Edward Dougherty, Center for Imaging Science, Rochester Institute of Technology, USA Murray Eden, Director of Biomedical Engineering, National Institutes of Health, Bethesda, USA Borko Furht, Department of Computer Sceince and Engineering, Engineering, Florida Atlantic University, USA Madan Gupta, Intelligent Research Laboratory, College of Engineering, University of Saskatchewan, Canada Wolfgang Halang, Faculty of Electrical Engineering, Fern Universitaet, Germany Gabor Herman, University of Pennsylvania, Philadelphia, USA Tadao Ichikawa, Faculty of Engineering, University of Hiroshima, Higashi-Hiroshima, Japan Hanjin Lee, Daewoo Electronics, Seoul, Korea Bob Loce, Corporate Research and Technology, Xerox Corporation, USA Mihai Nadin, MINDesign, USA Paolo Nesi, Dept of Systems and Informatics, Faculty of Engineering, University of Florence, Italy Mike Rodd, University of Wales at Swansea, UK Azriel Rosenfeld, Center for Automation Research, University of Maryland, College Park, USA Div Sinha, City University of New York - Staten Island, USA Hartwig Steusloff, Fraunhofer Institute, Germany Brian J. Thompson, University of Rochester, USA Stephen S. Wilson, Applied Intelligent Systems, Inc., Ann Arbor, USA Real-Time Imaging will be published by Academic Press in six bimonthly issues, commencing in February 1995. Free sample copies, when available, can be obtained from; Academic Press Marketing Department 24-28 Oval Road London NW1 7DX Tel: (0) 71 482 2893 Fax: (0) 71 267 0362 Email: rti@apuk.co.uk Editorial Policy Each original article will be independently reviewed by at least two appropriate referees. On average, a decision will be reached within 4-5 weeks of the receipt of the manuscript. To avoid delay, e-mail will be used wherever possible. Publication will follow within 12 to 16 weeks of the acceptance date, assuming the prompt return of proofs. All six issues in the first year will be sent to subscribers to CVGIP: Graphical Models and Image Processing. Real-Time Imaging Real-Time Imaging welcomes original papers in fundamental real- time imaging technologies and their application areas. The journal will focus on papers of an applied nature although survey and theoretical papers with practical results are welcome. Areas covered include image compression, target acquisition and tracking, remote control and sensing, image enhancement and filtering, networking for real-time imaging, advanced computer architectures, computer vision, optical measurement and inspection, and simulation Emphasis is placed on the application of real-time imaging in the following technologies; robotics, virtual reality, multimedia, medical imaging, industrial inspection, high-definition television, advanced simulators, computer-integrated manufacturing, and intelligent vehicles. Manuscript submission Authors should send a copy of their paper in LaTex or ASCII or other readable sources to jrti@fdu.edu Alternatively, one original manuscript and three complete copies should be sent to; Alexander Stoyenko Real-Time Imaging PO Box 668 Millwood New York 10546 USA. The submission of a manuscript will be taken to imply that the material is original and has not been submitted in equivalent form for publication elsewhere. Manuscripts are accepted for review on the understanding that all persons listed as authors have given their approval for the submission, and that any person cited as a source of personal communication has approved such citation. To speed handling, please supply your telephone, fax and e-mail address, together with your mailing address. Articles and other materials published in Real-Time Imaging represent the opinions of the authors, and should not be construed to reflect the opinions of the Editors or Publisher. Copyright permission Authors submitting a manuscript do so on the understanding that if it is accepted for publication, exclusive copyright in the article shall be assigned to the publisher. The publisher will not put any limitation on the personal freedom of the author to use material contained in the paper in other works. Manuscript preparation If the manuscript is being submitted in paper form, it should be typewritten, double-spaced with one inch margins on all sides, using 8 1/2 x 11 inch paper, one side only. Each page of the manuscript should be numbered, and illustrations, tables and listings should be attached separately at the end with an appropriate caption list. One illustration or table should appear per page. Articles should be concise and in English. An abstract must accompany each manuscript and should not normally exceed 200-500 words. It should be intelligible to the general reader without reference to the main text. No references or abbreviations should be used in the abstract. Style The journal will use the style described for IEEE transactions Tables and figures All figures must be cited in the text and the legends should be numbered consecutively with arabic numerals. Legends should be sufficiently detailed to allow understanding without reference to the text. One colour illustration per paper is permitted. Footnotes Footnotes should be used sparingly and indicated by consecutive numbers in the text. Acknowledgments should be included at the end of the text, and not as footnotes. References References should be numbered consecutively in the order in which they are first mentioned in the text in square brackets. If cited in tables or figure legends, references are to be numbered according to position in the manuscript. In the reference list, all authors should be cited. Corrections Authors are expected to correct and return page proofs to the Publisher within a week of receipt. Authors are responsible for the costs of changes, additions or corrections other than the printer's or publisher's errors, although the publisher may waive such charges. Reprints Authors will receive fifty offprints free of charge. Submission of manuscripts on disk Manuscripts on disk are also welcomed. Please supply a disk prepared on PC compatible or Apple Macintosh computers, along with the hard copy print out. Please ensure that the final version of the hard copy and the file on disk are identical. 5 1/4" or 3 1/2" sized disks and most word processing packages are acceptable, although any version of WordPerfect and Microsoft Word are preferred. ------------------------------------------------------------------------------ Message 9; Postmarked Thu Jul 14 05:31:20 1994 From: ken@minster.york.ac.uk Subject: WWW page for the Real-Time Systems Research Group at York There is a World Wide Web page for the Real-Time Systems Research Group at York. It contains a list of papers recently published by the group, and links to other WWW pages of interest to real-time researchers. It also gives access to the FTP site containing York real-time publications. The URL is: http://dcpu1.cs.york.ac.uk:6666/real-time Please contact me (Ken Tindell) if there are any problems or suggestions about this service. ---- Ken Tindell Internet : ken@minster.york.ac.uk Computer Science Dept., Local FTP site: minster.york.ac.uk University of York, Tel. : +44-904-433377 YO1 5DD, UK Fax. : +44-904-432767 WWW page : http://dcpu1.cs.york.ac.uk:6666 ------------------------------------------------------------------------------ Message 10; Postmarked Tue Sep 13 08:37:22 1994 From: "FORTE'94 Organization Committee" Subject: FORTE'94 - Completed Program / Registration Information FORTE'94 Seventh International Conference on FORMAL DESCRIPTION TECHNIQUES Berne, Switzerland, 4 - 7 October 1994 Sponsored by IFIP WG6.1 in cooperation with ACM SIGCOMM and IEEE Computer Society TC on Distributed Processing PROGRAM ---------------------------------------------------------------------- Apologies for receiving multiple copies! Please note: * early registration deadline: September 15, 1994 * complete listing of position statements * tentative listing of tool demonstrations ---------------------------------------------------------------------- FORTE'94 will be held in Berne, in the "Aula" of the main building of the University of Berne, Hochschulstr. 4, CH-3012 Berne, Switzerland, 4 - 7 October 1994. Conference rooms are wheel-chair accessible. Please indicate on the registration form whether you need special help. The conference offers the presentation of 24 research papers, 3 industrial usage reports, 12 position statements, 6 tutorials and a number of tool demonstrations. Tutorials will be held on October 4 only. Tool presentations will take place concurrently with the conference presentations on October 5 to 7. Invited talks will be given by Nancy Lynch (MIT), Leslie Lamport (DEC-SRC) and Gerard Holzmann (AT&T Bell Laboratories). FORTE'94 will address formal techniques applicable to Distributed Systems such as Estelle, Lotos, SDL, ASN.1, 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 Formal Techniques and will provide an excellent orientation for newcomers. FORTE'94 will be sponsored by IFIP WG6.1 in cooperation with ACM SIGCOMM and the IEEE Computer Society Technical Committee on Distributed Processing. Additional supporters are: Alcatel STR, Siemens-Albis, ASCOM, Sun Microsystems and Swiss Telecom as well as the non-corporate sponsors Beer-Brawand Fund and the Swiss National Science Foundation. Participants will receive participants' proceedings and tutorial notes, the final proceedings will be published by Chapman & Hall, the official publisher of IFIP WG6.1 proceedings, in early 1995. ------------------------------------------------------------------- Tuesday, October 4: Tutorial Day ====================================== Registration: 7:45 - 8:00 The tutorials will be presented in two parallel tracks. Coffee breaks and starting times of tutorials in different tracks are synchronized so that switching between tutorials is easily possible. Track 1: 8:00 - 12:30 (coffee break: 10:00 - 10:30) Formal methods for reactive systems, the comparative case study `production cell', Claus Lewerentz, Thomas Lindner, Forschungszentrum Informatik, Karlsruhe, Germany. Abstract: The Forschungszentrum Informatik (FZI) has initiated and coordinated a comparative case study in the field of reactive systems design. Several methods, among them SDL, Esterel, Lustre, StateCharts, and RAISE have been applied to develop control software for a real-world industrial production cell, enforcing a number of safety requirements. First, the task of the case study will be presented. The participants will be introduced into the problem. The main difficulties to safe control of the plant will be shown. The tutorial will present a survey on different styles of reactive systems design, explaining the different classes of methods using the case study as a running example. Advantages and limitations of the approaches are discussed. Different methods involve different approaches to system verification. The most important approaches to prove correctness will be presented, explained, and evaluated. Finally, the tutorial will report on lessons learned from the case study. The benefits and limitations of formal methods will be discussed, final conclusions will be drawn. The tutorial also offers a brief introduction into the field of formal methods and into the techniques employed in the presentation. However, it would be advantageous to know one formal description technique in some more detail. Track 2: 8:00 - 12:30 (coffee break: 10:00 - 10:30) An Overview of the UNITY Methodology: Theory and Application, Mark G. Staskauskas, Software Production Research Department, AT&T Bell Laboratories, USA. Abstract: UNITY is a formal methodology for the development of concurrent and parallel programs that was created by K.M. Chandy and J. Misra at the University of Texas at Austin. UNITY consists of a simple program notation based on Pascal-style multiple assignment statements, a specification notation based on temporal logic, and a proof system consisting of a small set of inference rules. In this tutorial, we will present a thorough overview of the UNITY program notation, specification logic and proof system. To illustrate the application of UNITY, we will also present a case study of a UNITY design of the I/O subsystem portion of the GCOS operating system. This example will provide tutorial attendees with a complete, step-by-step picture of how UNITY has been effectively used on an actual software project, including the development of an abstract mathematical model that captures relevant aspects of the system to be designed; a UNITY specification of desired properties of the system; construction of an abstract algorithm in the UNITY program notation and a proof of its correctness; and use of the abstract algorithm as a pseudocode skeleton on which the system implementation is based. Track 1&2: 12:30 - 14:00: Lunch Track 1: 14:00 - 16:00 A tutorial introduction to real-time CSP, Jim Davies, University of Reading, UK. Abstract: Real-time CSP is a language for modelling the behaviour of real-time systems. It can be used to specify the times at which interaction and communication may occur. It supports reasoning about the timing and duration of system states, and allows the user to calculate whether or not timing constraints will be met. This tutorial introduces the language of real-time CSP and explores its use as a descriptive tool. The intention is to provide the audience with a firm grasp of the basic language, and a useful perspective upon its development and application. Track 2: 14:00 - 16:00 A tutorial on formal methods and conformance in Open Distributed Processing, Howard Bowman, John Derrick, University of Kent, UK. Abstract: This tutorial describes the Open Distributed Processing (ODP) development model and conformance assessment methodology with particular emphasis on the use of formal methods in these activities. Firstly the ODP Reference Model is outlined. The ODP development process is then explained including a discussion on the use of formal methods within this methodology. The ODP conformance assessment methodology (which includes both testing and specification checking) is presented, with particular reference to the use of formal methods in preserving the consistency across viewpoints. Finally different formal methods are evaluated in the context of developing and assessing conformance to ODP systems. Track 1&2: 16:00 - 16:30: Coffee break. Track 1: 16:30 - 18:30 True Concurrency Models for LOTOS, Rom Langerak, University of Twente, The Netherlands. Abstract: True concurrency models offer an important alternative to interleaving semantics. In this tutorial we give an overview of several proposals for a true concurrency semantics for LOTOS: partially ordered traces, causality-based operational semantics, prime event structures, bundle event structures, and event traces. Firstly the motivation for true concurrency and the concept of partial orders will be explained. Then the above models will be presented in an intuitive way, by giving small examples rather than elaborate formal mathematics. This will allow a non-specialist (who might otherwise easily be confused by the existence of so many alternative models) to understand the different proposals in the light of practical applications. Track 2: 16:30 - 18:30 SDL combined with ASN.1 / OSI protocol specification using SDL, Anders Olsen, Tele Denmark Research, Denmark, Louis Verhaard, Lennart Mansson, Telia Research AB, Sweden, Jan Ellsberger, TeleLogic AB, Sweden. Joint tutorial, exact title and abstract to be provided. ------------------------------------------------------------------- Wednesday, October 5, 1994: Conference Presentations ==================================================== 8:00 - 8:45 Registration 8:45 - 9:00 Welcome 9:00 - 10:00 Invited talk: Proving Performance Properties (even Probabilistic Ones), Nancy Lynch (MIT). Abstract: Some new formal methods allow for systematic verification of time performance properties of concurrent systems that satisfy some basic timing assumptions. These methods are potentially of practical benefit in the validation of real-time process control and communication systems. This talk surveys some of these methods, including (a) nondetermininistic automaton models, (b) invariant and simulation methods for proving worst-case time bounds, (c) probabilistic automaton models, and (d) Markov-style proofs of probabilistic time bounds. These methods are well suited for (partial) mechanization. 10:00 - 10:30 Coffee break 10:30 - 11:30 Introduction to tool demonstrations. 11:30 - 12:30 Session 1: New Techniques Chair: N.N. Semantic-oriented description techniques for network management information modeling, Deh-Min Wu (Technical University of Berlin). A service request description language, C. Popien, B. Meyer (Aachen University of Technology). 12:30 - 14:00 Lunch 14:00 - 16:00 Session 2: Applications Chair: N.N. Modelization and verification of a multiprocessor realtime OS kernel, Thierry Cattel (National Reserarch Council of Canada). Design of operating systems using the F.D.T. ESTELLE, Oliverio Gonzalez, Victor G. Garcia, Miguel Riesco, (University of Oviedo), Enrique Vazquez (University of Madrid). The formalization and analysis of CCR protocol and service, Bairong Zhang, Alistair Munro, Michael Barton, (University of Bristol). On the formal specification and verification of network routing algorithms, Jim Davies (University of Reading), Matt Wallis (BNR Europe Limited). 16:00 - 16:30 Coffee break 16:30 - 18:30 Session 3: FDTs go commercial Chair: Harry Rudin, IBM Zurich Research, Switzerland. Part I: Industrial Usage Reports Validation of supplementary services in interoperability context, S. Le Bricquir (CAP SESA OUEST), A. Lauzanne (SETICS). FDT based development of an interworking unit between LANs and X.25 networks, J.C. Yelmo*, F.J. Carrasco**, C. Sanchez*, J.J. Gil**, C. Ramos*, M.I. Felipe** (* Technical University of Madrid, ** Telefonica I + D). Using formal specification and simulation: Practical experience with distributed applications, Willem Hengeveld, Peter van der Toorn (Bakkenist Management Consultants), Geert-Jan Houben (Eindhoven University of Technology). Part II: Panel discussion "FDTs go commercial". Panel chair: Harry Rudin. ---------------------------------------------------------------------------- Thursday, October 6, 1994: Conference Presentations =================================================== 8:00 - 10:00 Session 4: Verification Chair: Guenther Karjoth, IBM Zurich Research, Switzerland. Representation of process-gate nets in LOTOS and verification of LOTOS laws: the boolean algebra approach, Pim Kars (University of Twente). Reachable state space analysis of LOTOS specifications, A. Kerbrat (VERIMAG). An improvement in formal verification, Gerard J. Holzmann, Doron Peled (AT&T Bell Laboratories). Position statements: A modal based verification for LOTOS, Hacene Fouchal, Ana R. Cavalli (Institut National des Telecommunications). Tableau methods to decide strong bisimilarity on LOTOS proceses involving pure interleaving and enabling, A. Fantecchi*, S. Gnesi, R. Sacchelli (I.E.I. - C.N.R.) * also Univ. di Pisa. Simulator for LOTOS to study the independence and auality of events, B. Botma, R. Langerak (University of Twente). 10:00 - 10:30 Coffee break 10:30 - 12:30 Session 5: Verification and Real-Time Chair: N.N. Verifying ET-LOTOS programs with KRONOS, C. Daws, A. Olivero, S. Yovine (VERIMAG). Automatic verification of real-time communicating systems by constraint-solving, Wang Yi, Paul Pettersson, Mats Daniels (Uppsala University). Verifying timing properties of concurrent algorithms, Victor Luchangco, Ekrem Soeylemez, Stephen Garland, Nancy Lynch (MIT). Postition statements: Formal specification and analysis of an ISO communications protocol, J.R. Rowson, (University of London). Verification model reduction through abstractions, Jean Charles Gregoire (INRS-Telecommunications). Visual animation of LOTOS using SOLVE, K.J. Turner (University of Stirling), A. McClenaghan (Philips research Labs.). 12:30 - 14:00 Lunch 14:00 - 15:00 Invited talk: How Good is Your Specification Method? Leslie Lamport, (DEC-SRC). Abstract: Formal methods abound for specifying concurrent systems. Proponents of a method usually talk about what it does and ignore what it can't do. I will present and explain desiderata for a specification method. 15:15 Departure for conference excursion and banquet, return approximately at 23:30. ---------------------------------------------------------------------- Friday, October 7, 1994: Conference Presentations ================================================= 8:00 - 9:30 Session 6 (Part I): Semantics Chair: N.N. Relating maximality-based semantics to action refinement in process algebras, J.-P. Courtiat, D. E. Saidouni (LAAS-CNRS). An abstract interpreter for the specification language LOTOS, Franco Fiore, Fosca Giannotti (CNR). An attempt to embed a restricted version of SDL as a target language in Focus, Eckhardt Holz (Humboldt University), Ketil Stoelen (TU Muenchen). 9:30 - 10:00 Coffee break 10:00 - 11:30 Session 6 (Part II): Semantics Delayed choice: an operator for joining Message Sequence Charts, J.C.M. Baeten, Sjouke Mauw (Eindhoven University of Technology). Four issues concerning the semantics of Message Flow Graphs, Peter B. Ladkin (CRIN/INRIA Lorraine), Stefan Leue (University of Berne). Position Statements: Towards a formal computational model for distributed multimedia applications, Andreas Vogel (University of Queensland). Specification, detection and resolution of IN feature interactions with Estelle, J. Bredereke, R. Gotzhein (University of Kaiserslautern) Application of protocol synthesis technique to resolution of service interaction problem, Yoshiaki Kakuda, Hiroyuki Asada, Tohru Kikuno (University of Osaka) 11:30 - 12:30 Invited talk: Proving the Value of Formal Methods, Gerard J. Holzmann (AT&T Bell Laboratories). Abstract: The record of successful applications of formal verification techniques is slowly growing. Our ultimate aim, however, is not to perform small pilot projects that show that verification is sometimes feasible in an industrial setting; our aim must be to firmly integrate verification techniques into the software design cycle as a non-negotiable part of quality control. Ultimately, the sale of a non-verified piece of software, or the standardization of a non-verified protocol or algorithm for use on computing machinery, should be as unthinkable as the prescription of untested, and potentially harmful, drugs for use by humans. In the talk we take a snapshot of the state of the art in formal verification, and consider how well it has been integrated into industrial practice so far. For inspiration, we compare the current situation with other points in history where new technology threatened to replace old technology, only to discover how resilient an established practice can be, and how remarkably long it can manage hold out. To keep a mild sense of perspective, however, we will also briefly consider how badly mistaken some of the advocates of new technology have sometimes been, and how right the people were that stuck to the old ways just a little bit longer... 12:30 - 14:00 Lunch 14:00 - 16:00 Session 7: Testing and Performance Chair: N.N. A structural analysis approach to the evaluation of fault coverage for protocol conformance testing, Mingyu Yao, Alexandre Petrenko, Gregor v. Bochmann (University of Montreal). Test sequence generation using Estelle or SDL structure information, Marc Phalippou (France Telecom - CNET). Derivation of efficient implementations from formal descriptions - issues, methods and conformance, H. Kremer (University of Twente). Position statements: Stochastic process algebras: integrating qualitative and quantitative Modelling, J. Hillston (University of Edinburgh), H. Hermanns, U. Herzog, V. Mertsiotakis, M. Rettelbach (University of Erlangen-Nuernberg). A new approach to performance evaluation of formally specified protocols, Stefan Boehmer, Ralf Klafka (Aachen University of Technology). Integrated analysis of concurrent distributed systems using markovian process algebra, Marco Bernardo, Lorenzo Donatiello, Roberto Gorrieri (Universita di Bologna) 16:00 - 16:30 Coffee break 16:30 - 18:30 Session 8: Refinement Chair: N.N. Modelling techniques for evolving distributed applications, Y-J. Lin, R. Sekar (Bellcore), C.R. Ramakrishnan (SUNY). A synthesis algorithm of a protocol model from a single entity, Bhed Bahadur Bista*, Zixue Cheng**, Atsushi Togashi*, Norio Shiratori* (* Tohoku University, ** University of Aizu). A new distributed algorithm for implementation of LOTOS multi- rendezvous, Zi-xue Cheng, Tong-jun Huang (Aizu University), Norio Shiratori (Tohoku University). Stepwise transformations for fault-tolerant design of CCS processes, Tomasz Janowski (University of Warwick). 18:30 - 18:45 Closing Session ------------------------------------------------------------------------ Tool demonstrations (running concurrently with the conference presenations): An integrated tool environment for SDL'92, Joachim Fischer (Humboldt Universitaet Berlin). GEODE: The ultimate toolset for SDL & MSC engineering, Vincent Encontre (VERILOG). Presentation of DSS and DICOMP tools, B. Tampakas (Computer Technology Institute Patras). SaMsTaG - SDL and MSC based Test Case Generator, Daniel Toggweiler (University of Berne). SDT - The SDL Design Tool, Per Blysa (Telelogic AB). (Tentative listing) ------------------------------------------------------------------------ Conference Chairperson: Dieter Hogrefe (University of Berne, CH) Conference Organization Chairperson: Stefan Leue (University of Berne, CH) Program Committee: Paul Amer (University of Delaware, USA) Gregor v. Bochmann (University of Montreal, CDN) Tommaso Bolognesi (CNUCE, I) Ed Brinksma (University of Twente, NL) Ana Cavalli (INT, F) Jean-Pierre Courtiat (LAAS-CNRS, F) Piotr Dembinski (Polish Academy of Science, PL) Ove Faergemand (EURESCOM, D) Reinhard Gotzhein (University of Kaiserslautern, D) Dieter Hogrefe (University of Berne, CH) Gerard Holzmann (AT&T Bell Labs, USA) Jean-Pierre Hubaux (EPF Lausanne, CH) Toshihiko Kato (KDD, J) Jan Kroon (PTT Research, NL) Stefan Leue (University of Berne, CH) Luigi Logrippo (University of Ottawa, CDN) Nancy Lynch (MIT, USA) Lynn Marshall (BNR, CDN) Jan de Meer (GMD Fokus, D) Elie Najm (ENST, F) Linda Ness (Bellcore, USA) Ken Parker (Telecom Research Laboratory, AUS) Bjorn Pehrson (SICS, S) Claude Petitpierre (EPF Lausanne, CH) Juan Quemada (DIT ETSIT UPM, E) Harry Rudin (IBM Research, CH) Deepinder Sidhu (University of Maryland, USA) Richard Tenney (University of Massachusetts, USA) Ken Turner (University of Stirling, UK) Umit Uyar (CUNY, USA) Son Vuong (University of British Columbia, CDN) Organisation Team (all University of Berne, CH): Manuela Beck (general organization and registration) Lucia Engel (general organization and registration) Heike Horn (technical support for tool presentations) Sylvia Schaad (finances) Patrick Zumbrunn (general organization) Further Information: FORTE'94 Organization Committee, University of Berne, P.O. Box 900, CH-3000 Berne 9, Switzerland Tel.: +41 31 631 ~4994 (Dieter Hogrefe) ~4430 (Stefan Leue, Patrick Zumbrunn) ~3568 (Manuela Beck, Lucia Engel) ~8955 (Heike Horn) ~8957 (Sylvia Schaad) ~3965 (Fax) Email: forte94@iam.unibe.ch. To obtain additional information and latest news please login via ftp on host `siam.unibe.ch' (IP address 130.92.66.11) as user `anonymous' and give your email address as password, then get the appropriate file from directory `forte94' (for particular filenames see file `README'). -------------------------------------------------------------------- Miscellaneous Berne was founded in 1191 by Berchtold V, Duke of Zaehringen. It was extended in various stages. From the 14th to the 16th century Berne reached the zenith of its power. In 1528 a "high school" (seminary) was erected in the old "Barfuesserkloster" (monastery). Its purpose was to educate the clergy of the reformed church. The present University of Berne was founded in 1834. In 1848, Berne became the Federal Capital of Switzerland. Berne is the seat of the diplomatic corps and of several international organizations such as the Universal Postal Union and the International Railway Office. Economy in Berne includes a well-developed services sector, machine engineering, electrical equipment, rotary printing presses, metals, pharmaceuticals, textiles, food, chocolate, graphic industry, and telecommunications. Berne has retained its old-world charm. In no other medieval town has so large an area been totally preserved true to the original style as in Berne. Today the streets of Berne, with their old houses, corner bay windows, fountains, towers, alleys, arcades and cellars are still virtually the same as they were serveral centuries ago. With its 6 km/4 mi of arcades Berne can offer visitors the largest modern shopping area in a medieval setting in Europe. Because Berne is concentrated on the steep-sided peninsula surrounded by the meandering River Aare, visitors can find everything they want within a very small area. Berne enjoys a central-European continental climate, with average temperatures of around 10-16 C/50-61 F in autumn. Time zone: Central European time (CET = GMT plus 1 hour). Travel Information The best international air travel connections are via the Zurich and Geneva international airports. These airports are connected to Berne by convenient direct hourly train services (Geneva 120 min., Zurich 90 min.). In both cases trains leave inside the airport terminal building and deliver you directly to the central railway station at Berne. Visitors travelling to their departure airports by rail can check in their luggage at the station in Berne for any destination in the world. The Berne-Belp (9 km/6 mi) commuter airport offers some international connections (including London, Paris, Brussels) but requires a bus or taxi transfer to the city center. From Berne the traveller has direct connections with the international rail network, including TGV (Paris) and EuroCity trains. Berne is centrally located in Switzerland. Almost any place in Switzerland can be visited from Berne in half- or full-day excursions, and all of Switzerland is easily reachable by train. If you plan for an extension of your visit in Switzerland - the tourist office will be happy to assist you. The availability of parking spaces in Berne is very limited and parking garages are very expensive. Therefore, we strongly recommend to travel to Berne by public transportation. The extensive, modern public transportation network (busses, streetcars) offers visitors frequent connections from every part to the city or every other part. This means there are no problems transferring from the station to your hotel and from there to the conference venue by public transportation. If desired, a special-general ticket for unlimited travel on the whole network can be issued to conference participants. Accommodation Information Please arrange your room reservations directly with the Official Tourist Office and Convention Bureau of Berne using the included hotel reservation form. There are 4 categories of rooms available. Cat. I is a first class hotel, cat. II are middle class hotels, cat. III are tourist class hotels, and cat. IV are one- star hotels with running water in the rooms, bath/shower on the floor but outside the room. All of the hotels are within easy reach of the conference site. Prices indicated on the hotel reservation form are special congress rates and include breakfast, service and taxes. Hotel rooms have been reserved until September 1, 1994. Reservations received after September 1, 1994 will only be accepted on a space available basis at the conference rate. Please send or fax your hotel reservation form directly to the Official Tourist Office and Convention Bureau of Berne, address see on the form. In addition to the hotels there is also a youth hostel that offers convenient low-budget accommodation. Price per night with the mandatory youth hostel membership card (can be bought on site for CHF 30.-) is about CHF 15.- to 22.- , breakfast about CHF 6.-. Please arrange your reservation directly with: Youth Hostel SJH Weihergasse 4 CH-3000 Berne 12 Switzerland phone: +41-31-311 63 16, fax: +41-31-312 52 40. _______________________________________________________________________________ ------------------------------------------------------------------------------- REGISTRATION FORM FORTE'94 4-7 October 1994, Berne SWITZERLAND Please complete this form and send it by mail, fax or email to: FORTE'94 Organization Committee University of Berne P.O. Box 900 CH-3000 Berne 9 Switzerland Tel.: (+41) 31 631 35 68 or 631 89 57 Fax.: (+41) 31 631 39 65 email: forte94@iam.unibe.ch _________________________________________________________ I will attend the FORTE'94 meeting in Berne. Name____________________________________________________ First Name______________________________________________ Address_________________________________________________ ZIP/Postal Code___________City__________________________ Country_________________________________________________ Affiliation_____________________________________________ Phone___________________________________________________ Fax_____________________________________________________ Email___________________________________________________ Date_______________Signature____________________________ Your name as it should appear on your badge: ________________________________________________________ REGISTRATION FEES All fees in Swiss Francs (CHF). Early registration deadline is September 15, 1994 Type of Early Late Fee registration Calculation Tutorial: CHF 320,00 CHF 420,00 _________ Conference: CHF 590,00 CHF 700,00 _________ Full: CHF 730,00 CHF 850,00 _________ Student(1): CHF 350,00 CHF 400,00 _________ Total fee CHF ========= Tutorial registration fee covers: Attendance of tutorials, tutorial notes, lunch and coffee breaks on October 4, 1994 Conference registration fee covers: Conference admission, participant's proceedings, lunches, coffee breaks and the conference banquet dinner. Full or Student(1) registration fees cover: Attendance of tutorials and conference, tutorial notes, participant's proceedings, lunches, coffee breaks and the banquet dinner. (1) Please attach proof of student status. Methods of payment: I would like to pay the registration fee for FORTE'94 ___ ___ by |___| credit card: |___| Visa ___ |___| MasterCard/Eurocard ___ |___| American Express Name on the credit card: ______________________________ Credit card number: ______________________________ Expiration date: ______________________________ Authorized signature: ______________________________ ___ by |___| cheque: in CHF drawn on a Swiss Bank, payable to FORTE'94, Berne, Switzerland, fees to be charged to the issuer of the cheque. ___ by |___| money transfer on the account of FORTE'94, Swiss Bank Corporation, Berne, Switzerland, account 90-229.625.0. If you cancel, we must receive your cancellation by mail, fax or email by September 19, 1994. You will be charged a CHF 100.- handling fee. If you cancel after September 19, 1994, the full registration fee is due! Please specify your dietary requirements for lunch and banquet dinner: __________________________________________________________ Please specify whenever you need special help: __________________________________________________________ Official Conference Airline Swissair is the official conference airline and supports FORTE'94. ___ |___| I wish NOT to be contacted by a SWISSAIR agent for travel information. _______________________________________________________________________________ ---------------------------------------------------------------------------- Hotel Reservation FORTE'94 4-7 October 1994 Berne, Switzerland ______________________________________________________________________________ You can choose between the following categories of rooms: Cat. I. Cat. II Cat. III Cat IV Single room with bath/shower CHF 143.- CHF 122.- CHF 82.- CHF 60.- Twin-bedded room with bath/shower CHF 180.- CHF 155.- CHF 112.- Prices are indicated per night and include breakfast, taxes and service. Prices for rooms in different categories are guaranteed. However, the number of rooms per category is limited. Therefore, we recommend early reservation. After September 1, 1994, rooms can only be reserved on a space-available basis. The bill is to be paid by the guest directly to the hotel when checking out. I would like to stay in a hotel of category _ _ _ _ |_| I, |_| II, |_| III, |_| IV (please check). I need a _ |_| single room, _ |_| twin-bedded room (please check). Date of arrival_____________Date of departure___________ I need the room for ______ nights. ___ I will arrive |___| by car ___ |___| by train ___ |___| by airplane You will receive a written confirmation (mail or fax). Name____________________________________________________ First Name______________________________________________ Address_________________________________________________ ZIP/Postal Code___________City__________________________ Country_________________________________________________ Phone___________________________________________________ Fax_____________________________________________________ Date___________________Signature________________________ Please send this form by mail to the Official Tourist Office and Convention Bureau of Berne, FORTE'94, P.O. Box, CH-3001 Berne, Switzerland. Or fax it to +41 31 312 12 33. Please note that FORTE'94 is not your contractual partner for your hotel reservations. ------------------------------------------------------------------------------ ------------------------------------------------------------------------------ <<<<<<<<<<<<<<<<<<<* END OF THE IEEE-CS TC-RTS NEWSLETTER *>>>>>>>>>>>>>>>>>>> ------------------------------------------------------------------------------ The TC-RTS repository is maintained by Azer Bestavros at Boston University Internet address for anonymous FTP to the TC-RTS repository is: cs.bu.edu Contributions to this forum should be sent via E-mail to: IEEE-RTTC@cs.bu.edu Requests / inquiries should be sent via E-mail to: IEEE-RTTC-request@cs.bu.edu ------------------------------------------------------------------------------