Subject: IEEE-CS TC-RTS Newsletter for Tue Jul 12, 1994 _______________________________________________________________________________ __ _ __ ___ ___ __ __ I E E E Technical Committee |\ | |_ | | (_' | |_ | | |_ |_) C S on Real-Time Systems | \| |__ |/\| ,_) |__ |__ | | |__ | \ _______________________________________________________________________________ Table of Contents Line ----------------- ---- 1. Sergio.Yovine@imag.fr (98 lines) Automatic Verification Tools---additional entry.................... 2 2. Lars-}ke Fredlund (770 lines) CONCUR'94 Programme and Call for Registration...................... 100 3. JUK@vtttko.tko.vtt.fi (Jukka Karjalainen VTT Electronics (228 lines) Cfp: Euromicro workshop on Real-time Systems 1995.................. 871 4. lwelch%gollum@relay.nswc.navy.mil (Lonnie Welch) (163 lines) 3rd Workshop on Parallel and Distributed Real-Time Systems......... 1099 5. son@bbibbi.cs.virginia.edu (98 lines) ISMM Conference on Intelligent Information Management Systems ..... 1262 ------------------------------------------------------------------------------ <<<<<<<<<<<<<<<<<<* START OF THE IEEE-CS TC-RTS NEWSLETTER *>>>>>>>>>>>>>>>>>> ------------------------------------------------------------------------------ Message 1; Postmarked Mon Jun 27 10:42:43 1994 Subject: Automatic Verification Tools---additional entry From: Sergio.Yovine@imag.fr \documentstyle{article} \newcommand{\Kronos}{{\sc Kronos}} \newcommand{\CTL}{{\sc Ctl}} \newcommand{\TCTL}{{\sc Tctl}} \title{Kronos: A Tool for Verifying Real-time Systems} \author{A. Olivero and J. Sifakis and S. Yovine\\ VERIMAG-SPECTRE \thanks{VERIMAG is a joint laboratory of CNRS, INPG, UJF and VERILOG S.A., associated with Institut IMAG. SPECTRE is an INRIA project.}} \begin{document} \maketitle \section{Description of the tool} \Kronos\ is a tool that performs {\em symbolic model checking\/} for real-time systems. It reads a {\em timed graph\/} describing a real-time system and a \TCTL\ formula specifying a requirement, and checks whether the timed graph satisfies the formula. Timed graphs are automata extended with a finite set of real-valued {\em clocks}, used to express timing constraints. Clocks can be set to zero and their values increase uniformly with time. At any instant the value of a clock is equal to the time elapsed since the last time it was reset. A transition is enabled only if the timing constraint associated with it is satisfied by the current values of the clocks. Many slightly different definitions of timed graphs exist, see for instance~\cite{rtl:acd90,atp:ieee}. \Kronos\ adopts the definitions given in~\cite{atp:ieee}. \TCTL\ is a real-time temporal logic. \TCTL\ is an extension of \CTL\ that permits quantitative temporal reasoning. Various definitions of \TCTL\ have been given, see for instance~\cite{rtl:acd90,rtl:lics92}. \Kronos\ adopts the definition given in~\cite{rtl:acd90} where temporal operators have subscripts that limit their scope in time. \Kronos\ implements the symbolic model-checking algorithm developed in~\cite{rtl:lics92,rtl:ic94}. \section{How to get it} \Kronos\ is distributed free of charge to universities and academic research centers. It can be obtained by sending an e-mail request to Sergio.Yovine@imag.fr. Related articles and reports can be obtained by anonymous ftp from imag.fr in the directory /pub/SPECTRE/KRONOS/articles. For further information please contact: \begin{center} Sergio Yovine\\ VERIMAG\\ Miniparc - Zirst\\ Rue Lavoisier\\ 38330 Montobonnot St. Martin\\ FRANCE\\ Tel: +33 76 90 96 41\\ Fax: +33 76 41 36 20\\ E-mail: Sergio.Yovine@imag.fr. \end{center} \begin{thebibliography}{HNSY94} \bibitem[ACD90]{rtl:acd90} R.~Alur, C.~Courcoubetis, and D.~Dill. \newblock Model-checking for real-time systems. \newblock In {\em Proc. 5th Symp. on Logics in Computer Science}, pages 414--425. {IEEE} Computer Society Press, 1990. \bibitem[HNSY92]{rtl:lics92} T.A. Henzinger, X.~Nicollin, J.~Sifakis, and S.~Yovine. \newblock Symbolic model-checking for real-time systems. \newblock In {\em Proc. 7th Symp. on Logics in Computer Science}. {IEEE} Computer Society Press, 1992. \bibitem[HNSY94]{rtl:ic94} T.~Henzinger, X.~Nicollin, J.~Sifakis, and S.~Yovine. \newblock Symbolic model-checking for real-time systems. \newblock {\em Information and Computation}, to appear, 1994. \bibitem[NSY92]{atp:ieee} X.~Nicollin, J.~Sifakis, and S.~Yovine. \newblock Compiling real-time specifications into extended automata. \newblock {\em {IEEE TSE} {S}pecial {I}ssue on {R}eal-{T}ime {S}ystems}, 18(9):794--804, September 1992. \end{thebibliography} \end{document} ------------------------------------------------------------------------------ Message 2; Postmarked Tue Jun 14 09:55:13 1994 Subject: CONCUR'94 Programme and Call for Registration From: Lars-}ke Fredlund CONCUR'94 Fifth International Conference on Concurrency Theory August 22 - 25 1994 Uppsala, Sweden PROGRAMME and CALL FOR REGISTRATION AIM CONCUR'94 is the Fifth International Conference on Concurrency Theory. The basic aim of the CONCUR conferences is to communicate advances in concurrency theories and applications. The first two meetings were held in Amsterdam in August 1990 and 1991, the third in Stony Brook, New York, U.S.A., in August 1992, and the fourth meeting was held in Hildesheim, Germany, in August 1993. The proceedings of these conferences have appeared in Springer-Verlag's Lecture Notes in Computer Science series as volumes 458, 527, 630, and 715, and the proceedings of CONCUR '94 will appear in the same series. The programme of CONCUR '94 includes presentations of selected papers, invited presentations, and tutorials. We also welcome participants to bring and demonstrate software packages that are relevant to the aims of the conference. More information regarding demonstrations is available later in this programme. VENUE The conference will be held at ``Folkets hus'' in central Uppsala, from which many tourist attractions are within walking distance. Accommodation will be close to the conference site. Uppsala is situated 70 km north of Stockholm, and can be conveniently reached from Stockholm Arlanda airport, which is situated 35 km south of Uppsala. PROGRAMME COMMITTEE Ralph-Johan Back, Jos Baeten, Eike Best, Ed Clarke, Mads Dam, Rob van Glabbeek, Cliff Jones, Bengt Jonsson (organising committee chair), Kim Larsen, Ugo Montanari, Mogens Nielsen, Catuscia Palamidessi, Joachim Parrow (program committee chair), Scott Smolka, Bernhard Steffen, Colin Stirling, P.S. Thiagarajan, Frits Vaandrager, Pierre Wolper, and Zhou Chaochen. INVITED SPEAKERS David Dill (Stanford University, USA), Jean-Yves Girard (CNRS, France), Paris Kanellakis (Brown University, USA), Mogens Nielsen (University of Aarhus, Denmark), and Prakash Panangaden (McGill University, Canada). TUTORIAL LECTURES Ralph-Johan Back (]bo Akademi, Finland), Costas Courcoubetis (Institute of Computer Science, FORTH, and University of Crete, Greece), Jean-Claude Fernandez and Joseph Sifakis (VERIMAG, France), and Robert de Simone (INRIA, France). DEMOS We invite participants to organise demonstrations. Sun workstations will be available at the conference site. Please contact Anders Andersson (e-mail: concur94-demo@docs.uu.se) well in advance to settle issues concerning requirements and installation, so that software packages can be transferred and installed in due time. SPONSORS Support for CONCUR '94 has been generously provided by: Ericsson Telecom Telia Research The Wenner-Gren Scientific Foundation The Swedish National Board for Industrial and Technical Development The Swedish Research Council for Engineering Sciences The Swedish Natural Science Research Council SCIENTIFIC PROGRAMME Sunday, August 21 19:00-21:00 Welcome Reception at ``Folkets Hus'' Monday, August 22 8:00- Registration 8:45-9:00 Welcome 9:00-10:00 Invited Lecture: Geometry of interaction J.-Y. Girard (CNRS, France) 10:00-10:30 A compositional semantics for Statecharts using labeled transition systems A.C. Uselton and S.A. Smolka(State University of New York at Stony Brook, USA) 10:30-11:00 Coffee and refreshments 11:00-11:30 On the decidability of non-interleaving process equivalences A. Kiehn (TU Munchen, Germany) and M. Hennessy (University of Sussex, England) 11:30-12:00 Regularity of BPA-systems is decidable S. Mauw and J.C. Mulder (Eindhoven University of Technology, The Netherlands) 12:00-12:30 A fast algorithm for deciding bisimilarity of normed context-free processes Y. Hirshfeld (Tel Aviv University, Israel) and F. Moller (SICS, Sweden) 12:30-14:00 Lunch 14:00-15:30 Tutorial: Model-based verification methods and tools J.C. Fernandez (VERIMAG, France), J. Sifakis (VERIMAG, France) and R. de Simone (INRIA, France) The tutorial is accompanied by a hands-on section, which can be completed by attendees during the remaining conference on the available Sun workstations. 15:30-16:00 New results in the analysis of concurrent systems with an indefinite number of processes M. Girkar and R. Moll (University of Massachusetts, USA) 16:00-16:30 Coffee and refreshments 16:30-17:00 Verification of nonregular temporal properties for context-free processes A. Bouajjani (VERIMAG, France), R. Echahed (LGI-IMAG, France) and R. Robbana (VERIMAG, France) 17:00-17:30 Pushdown processes: parallel composition and model checking O. Burkart (RWTH Aachen, Germany) and B. Steffen (Universit{t Passau, Germany) 17:30-18:00 Local model checking for parallel compositions of context-free processes H. Hungar (University of Oldenburg, Germany) 18:30- Reception in the main university building Tuesday, August 23 8:30-9:30 Invited Lecture: The logical structure of concurrent constraint programming languages P. Panangaden (McGill University, Canada) 9:30-10:00 Countable non-determinism and uncountable limits P. Di Gianantonio, F. Honsell and S. Liani (Universita di Udine, Italy), G. Plotkin (University of Edinburgh, Scotland) 10:00-10:30 SProc categorically J.R.B. Cockett and D.A. Spooner (University of Calgary, Canada) 10:30-11:00 Coffee and refreshments 11:00-12:30 Tutorial: From timed graphs to hybrid automata C. Courcoubetis (FORTH, and University of Crete, Greece) 12:30-14:00 Lunch 14:00-15:00 Invited Lecture: Hierarchical models of synchronous circuits D. Dill (Stanford University, USA) 15:00-16:00 The observational power of clocks R. Alur (AT&T Bell Laboratories, USA), C. Courcoubetis (FORTH and University of Crete, Greece) and T.A. Henzinger (Cornell University, USA) 15:30-16:00 A dynamic approach to timed behaviour J. Gunawardena (Hewlett-Packard, USA) 16:00-16:30 Coffee and refreshments 16:30-17:00 Algebras of processes of timed Petri nets J. Winkowski (Instytut Podstaw Informatyki PAN, Poland) 17:00-17:30 Operational semantics for the Petri box calculus M. Koutny (University of Newcastle upon Tyne, England), J. Esparza (University of Edinburgh, Scotland) and E. Best (Universit{t Hildesheim, Germany) 17:30-18:00 Weak sequential composition in process algebras A. Rensink and H. Wehrheim (Universit{t Hildesheim, Germany) Wednesday, August 24 8:30-9:30 Invited Lecture: Efficient parallelism vs reliable distribution: a tradeoff for concurrent computations P. Kanellakis (Brown University, USA) 9:30-10:00 On unifying assumption-commitment style proof rules for concurrency Q. Xu (]bo Akademi, Finland), A. Cau (Christian-Albrechts Universit{t zu Kiel, Germany) and P. Collette (Universite Catholique de Louvain, Belgium) 10:00-10:30 Liveness and fairness in Duration calculus J.U. Skakkebaek (Technical University of Denmark) 10:30-11:00 Coffee and refreshments 11:00-11:30 A symbolic semantics for the pi-calculus M. Boreale and R. De Nicola (Universita di Roma ``La Sapienza'', Italy) 11:30-12:00 On bisimulation in the pi-calculus D. Walker (University of Warwick, England) 12:00-12:30 Characterizing bisimulation congruence in the pi-calculus X. Liu (University of Sussex, England) 12:30-14:00 Lunch 14:00-14:30 The limit view of infinite computations N. Klarlund (University of Aarhus, Denmark) 14:30-16:00 Tutorial: Trace Refinement of Action Systems R.J.R. Back (]bo Akademi, Finland) 16:30- Excursion and Conference Dinner Thursday, August 25 8:30-9:30 Invited Lecture: Bisimulation for models in concurrency M. Nielsen (University of Aarhus, Denmark) 9:30-10:00 Invariants in process algebra with data M.A. Bezem and J.F. Groote (Utrecht University, The Netherlands) 10:00-10:30 Testing-based abstractions for concurrent systems R. Cleaveland (North Carolina State University, USA) and J. Riely (University of North Carolina, USA) 10:30-11:00 Coffee and refreshments 11:00-11:30 A congruence theorem for structured operational semantics with predicates and negative premises C. Verhoef (Eindhoven University of Technology, The Netherlands) 11:30-12:00 Deriving complete inference systems for a class of GSOS languages generating regular behaviours L. Aceto (University of Sussex, England) 12:00-12:30 Process algebra with partial choice J.C.M. Baeten (Eindhoven University of Technology, The Netherlands) and J.A. Bergstra (University of Amsterdam and Utrecht University, The Netherlands) 12:30-14:00 Lunch 14:00-14:30 Probabilistic simulations for probabilistic processes R. Segala and N. Lynch (Massachusetts Institute of Technology, USA) 14:30-15:00 Fully abstract characterizations of testing preorders for probabilistic processes S. Yuen (Nagoya University, Japan), R. Cleaveland (North Carolina State University, USA), Z. Dayar (North Carolina State University, USA) and S.A. Smolka (State University of New York at Stony Brook, USA) 15:00-15:30 Composition and behaviors of probabilistic I/O automata S.-H. Wu, S.A. Smolka and E.W. Stark (State University of New York at Stony Brook, USA) ABSTRACTS FOR TUTORIAL PROGRAMME Model-Based Verification Methods and Tools J. C. Fernandez, J. Sifakis (VERIMAG, France), R. de Simone (INRIA, France) Monday, August 22, 14:00 - 15:30 We describe established verification methods in the framework of communicating concurrent systems, focusing on model-based approaches implemented by existing tools for automatic verification. Such tools can be sorted by several features: input description language, specification style for properties (temporal logic vs operational behaviour), type of interpretation (linear time vs branching time). In contrast, most share the same modeling into labeled transition systems. In addition to the techniques of model-checking (or satisfaction of a temporal logic formula by a model) and model comparison (by behavioural equivalence or behavioural inclusion), we also present several methods for model simplification (abstraction, quotient minimisation,...). In all cases we face the issues of algorithmic complexity, of expressivity, and also of clarity and simplicity of usage. We end with an extensive description of the verification tools Aldebaran and Auto developed in our groups, followed by a tentative hands-on session for the attendees. >From Timed Graphs to Hybrid Automata Costas Courcoubetis (Institute of Computer Science, FORTH, and University of Crete, Greece) Tuesday, August 23, 11:00 - 12:30 We discuss various automata-theoretic formalisms for the specification and verification of real-time systems. We start with the general formalism of the hybrid automata as a model and specification language for hybrid systems. This is an extension of the traditional automata on infinite words in which the behavior of variables is governed in each state by a set of differential equations. Then we introduce the models of the timed automata and the integration graphs as special cases of the hybrid automata. We discuss the complexity of important verification issues related to the above models such as reachability and model-checking, and we survey the related algorithms. Trace Refinement of Action Systems Ralph-Johan Back (]bo Akademi University, Turku, Finland) Wednesday, August 24, 14:30 - 16:00 Action systems provide a general description of reactive systems, capable of modeling terminating, aborting and infinitely repeating systems. Arbitrary sequential program statements can be used to describe the behavior of atomic actions. Action systems are used to extend the Refinement Calculus, originally designed for sequential program refinement, to handle refinement of parallel and reactive systems. This permits systems to be built in which sequential and parallel constructs can be arbitrarily nested within each other. We will describe a behavioral semantics for action systems, in terms of execution traces, and define refinement of action systems based on this semantics. We show that trace refinement is a special case of data refinement of sequential programs. We give a general proof rule for action system refinement in a reactive context. This general proof rule can be shown both sound and complete for trace refinement under certain rather reasonable restrictions. Forward and backward simulation proof methods both arise as special cases of this general rule. We show how to derive specialized versions of these proof rules to handle situations that arise often in practical applications. We illustrate the use of reactive system refinement with an example. (Joint work with J. von Wright) ABSTRACTS OF INVITED LECTURES Geometry of Interaction Jean-Yves Girard (CNRS, France) Monday, August 22, 09:00 - 10:00 Geometry of Interaction is based on the idea that the ultimate explanation of logical rules is through the cut-elimination procedure. This is achieved by means of a pure geometric interpretation of normalization~: o proofs are operators on the Hilbert space describing I/O dependencies o cut-elimination is the solution of an I/O equation \[U(x \oplus \sigma(a)) = y \oplus a\] (the cut $\sigma$ expressing a feedback of some output of the proof U to some input of U) o termination is nilpotency of the operator $\sigma U$ o execution is expressed by \[RES (U,\sigma) := (1-\sigma^2)U(1-\sigma U)^{-1}(1-\sigma^2)\] This interpretation is available for full linear logic, which means, using translations for all constructive logics, in particular for typed lambda-calculi. It also works for untyped calculus, modulo a slight weakening of the hypotheses, expressing the absence of deadlock. Geometry of Interaction expresses a pure local asynchronous form of execution. Among the distinguished features of this execution, let us mention the distinction between public and private data... By the way there are two ways to combine operators in a way respecting privacy, and these two ways correspond to the two conjunctions of linear logic. The Logical Structure of Concurrent Constraint Programming Languages Prakash Panangaden (McGill University, Canada) Tuesday, August 23, 08:30 - 09:30 The Concurrent Constraint Programming paradigm has been the subject of growing interest as the focus of a new paradigm for concurrent computation. Like logic programming it claims close relations to logic. In fact these languages are logics in a certain sense that we make precise. In recent work it was shown that the denotational semantics of determinate concurrent constraint programming languages forms a categorical structure called a hyperdoctrine which is used as the basis of the categorical formulation of first order logic. What this connection shows is the combinators of determinate concurrent constraint programming can be viewed as logical connectives. In the present work we extend these ideas to the operational semantics of these languages and thus make available similar analogies for the indeterminate concurrent constraint programming languages. We also describe a linear extension of concurrent constraint programming and discuss hyperdoctrines for such languages. The discussion concludes with an examination of the prospects for understanding other formalisms for concurrent computation in the same way. One need never have heard of a hyperdoctrine in order to follow the talk. (Joint work with N. Mendler, P. Scott and R. Seely) Hierarchical Models of Synchronous Circuits David Dill (Stanford University, USA) Tuesday, August 23, 14:00 - 15:00 We seek a behavioral model of synchronous circuit operation which generalizes Mealy machines in several ways: o It should allow the expression of nondeterministic behavior. o It should allow parallel composition of machines and hiding of output signals. o It should not restrict bidirectional communication between machines. o It should deal reasonably with zero-delay cycles, which can be present in unrestricted communication graphs. o It should provide a preorder that precisely captures the proper relationship between implementation and specification behaviors. o It should allow the computation of the "most general environment" of a circuit. Surprisingly, given the attention that has been paid to switching theory over the years, no adequate model exists meeting these criteria. Devising such a model is more challenging than we had expected. This talk is a description of several of the specific problems that arise, along with solutions to some of them. Efficient Parallelism vs Reliable Distribution: a Tradeoff for Concurrent Computations Paris Kanellakis (Brown University, USA) Wednesday, August 24, 08:30 - 09:30 Concurrent computations should combine efficiency with reliability, where efficiency is usually associated with parallel and reliability with distributed computing. Such a desirable combination is not always possible, because of an intuitive tradeoff: efficiency requires removing redundancy from computations whereas reliability requires some redundancy. We survey a spectrum of algorithmic models (from fail-stop, synchronous to asynchronous and from exact to approximate computations) in which reliability is guaranteed with small tradeoffs in efficiency. We illustrate a number of cases where optimal tradeoffs are achievable. A basic property of all these models (of some interest in the study of concurrency) is that ``true'' read/write concurrency is necessary for fault tolerance. In particular, we show how algorithms can be designed so that, in each execution, the total concurrency used can be closely related to the faults that can be tolerated. (Joint work with D. Michailidis and A. Shvartsman) Bisimulation for Models in Concurrency Mogens Nielsen (University of Aarhus, Denmark) Thursday, August 25, 08:30 - 09:30 Recently, Joyal, Nielsen and Winskel suggested a categorical definition of bisimulation, applicable to a wide range of models for concurrency with an accompanying notion of observations. The definition is in terms of span of open maps, and it coincides with Milner's strong bisimulation for the standard model of labelled transition systems with sequential observations. In this talk we investigate this categorical notion of bisimulation for a selection of alternative models and observations (like Petri Nets with nonsequential observations), focusing on game theoretical and logical characterizations. GENERAL INFORMATION Conference Venue The conference will be held in the conference facilities in ``Folkets Hus'', Dragarbrunnsgatan 46, in central Uppsala. The majority of accommodation possibilities are located within a 1-15 minute walk from the conference site. Uppsala, situated 70 km north of Stockholm, is the fourth largest city in Sweden with almost 160.000 inhabitants and a decidedly academic atmosphere. Uppsala University, founded in 1477, is the oldest university in Scandinavia and has more than 20.000 students. The weather in Uppsala in August is warm, with a temperature around 15-20 degrees Celsius (60-70 Fahrenheit), ranging between very sunny and rain. A pullover and a raincoat or umbrella can at times be useful. Travel Information Uppsala can be conveniently reached from Stockholm Arlanda airport, which is situated 35 km south of Uppsala. Stockholm Arlanda airport is served by most major airlines. There is a regular bus service (No. 801) directly from the airport to Uppsala city centre every half hour. There are train connections between Stockholm and Uppsala every hour (50 minute ride). From Stockholm, it takes approximately 45 minutes along highway E4 to reach Uppsala by car. Registrants will receive detailed travel information with their confirmation. Registration Please register for CONCUR'94 by sending the attached registration and accommodation form to the Conference Secretariat, by regular mail or fax (see later page} for address information). Note that forms cannot be sent by e-mail. Fees, all indicated in Swedish crowns (SEK), are as follows. before July 15 after July 15 Regular fee SEK 1.700 SEK 2.200 Student fee SEK 900 SEK 1.100 The regular fee includes attendance to all sessions, a copy of the proceedings, conference dinner, lunches, refreshments, and excursion. The reduced student fee includes the same benefits as the regular fee except for the conference dinner and excursion, which have to be paid for separately (500 SEK) when applying for the student fee. The same extra fee for the conference dinner and excursion applies for accompanying persons. Requests for refunds will be honoured until August 1, except for an administrative fee of SEK 400. The registration should reach Uppsala Turist & Kongress NO LATER THAN JULY 15!!! Payments All payments are to be made in SEK. Please effect payment either o By Postal Giro to No. 19 57 52 - 1, Uppsala Turist & Kongress, mark payment ``CONCUR 94''. o By international money order, payable to Uppsala Turist & Kongress, mark payment ``CONCUR 94'' (note that personal checks will not be accepted). o By money transfer to: Foereningsbanken Uppsala, No. 7124-12-773 70, Box 276, S - 753 22 Uppsala, Sweden. o By credit card: American Express, Visa, Master Card, and Eurocard are accepted. Accommodation To reserve your accommodation, please fill in the Hotel Reservations section on the registration form and return it to the Conference Secretariat (see later page for address information), preferably no later than July 15, 1994. We have made preliminary reservations until July 15 in Hotel Svava and Hotel Linne in central Uppsala. A less expensive alternative is Samariterhemmet, a guest house with limited service. Still cheaper are rooms in private apartments (Bed and Breakfast style) which can be reserved through the conference registration service (Uppsala Turist & Kongress). Prices are as follows: Hotel Single room/night Double room/night Svava SEK 675 SEK 800 Linne SEK 650 SEK 850 Samariterhemmet (limited supply) SEK 430 SEK 650 Private room (B&B) SEK 190 (1st night) SEK 190 (1st night) SEK 150(from 2nd night) SEK 150 (from 2nd night) If you wish to share a room, please indicate the name of your room-mate. Meals Coffee Breaks, and Lunches will be served at the conference site. Lunches are served in the ``Winter Garden'' of ``Folkets Hus''. Social Events A reception preceding the conference will be held in the conference facilities on Sunday, August 21 at 19.00. A reception and welcome by Uppsala University will be held in the main university building on Monday, August 22 at 18.30. Excursion and conference dinner are combined in a boat trip on Lake M{laren from Uppsala to Skokloster Castle, a 17th century palace, with one of the largest collections of weaponry in the world. The castle is one of the most splendid examples of Swedish 17th-century county estate architecture and is very well preserved. The boat leaves on Wednesday, August 24 at 16.30. Currency Information The currency in Sweden is the Swedish Crown (SEK). The exchange rate (in May 1994) is approximately 7.8 SEK for 1 US$. All major credit cards are generally accepted in hotels, restaurants, shops, etc. Conference and Hotel Registration should be directed to the Conference secretariat: CONCUR '94 Uppsala Turist & Kongress Fyris Torg 8, S-753 10 Uppsala, Sweden. Tel: +46 - 18 - 27 48 08 Fax: +46 - 18 - 69 24 77 Correspondence on Other Matters should be directed to the Scientific secretariat: CONCUR '94 c/o Dept. of Computer Systems Uppsala University Box 325, S-751 05 Uppsala, Sweden Tel: +46 - 18 - 18 30 21 Fax: +46 - 18 - 55 02 25 e-mail:concur94@docs.uu.se Electronic Conference Information is available: For anonymous FTP users: host FTP.DoCS.UU.SE file docs/concur94/program.{txt,tex,dvi,ps} For WWW users: http://WWW.DoCS.UU.SE/concur94 For Gopher users: HOST=gopher.DoCS.UU.SE PORT=70 PATH=1/eng/docs/concur94 TYPE=1 NAME="CONCUR '94 conference" Conference jointly organised by: Dept. of Computer Systems, Uppsala University Swedish Institute of Computer Science Dept. of Teleinformatics, Royal Institute of Technology CUT HERE FOR REGISTRATION FORM REGISTRATION FORM Concur'94 - Fifth International Conference on Concurrency Theory, Uppsala, Sweden, August 22-25, 1994 Please type or use capital letters! REGISTRATION Family name:_______________________ First name:___________________________ Affiliation:_____________________________________________Title:___________ Address(work):____________________________________________________________ Code/City:_________________________ Country:______________________________ Telephone:_________________ Fax:________________ E-mail:__________________ Name(s) of accomp. person(s): ____________________________________________ REGISTRATION FEES Before July 15 After July 15 SEK Participant 1.700 SEK 2.200 SEK _______ Student 900 SEK 1.100 SEK _______ SOCIAL PROGRAMME Excursion to Skokloster Castle by Boat, Wednesday August 24. No. of Persons Participants 0 Students/Accompanying Persons 500 SEK/person} _______ TOTAL FEE(registation + Social programme) _______ PAYMENT Indicate which of the following means of payment you will use: 1. ____ Postal Giro No. 19 57 52-1, Uppsala Turist & Kongress, Sweden. 2. ____ International money order payable to Uppsala Turist & Kongress, ``CONCUR-94'', Fyris Torg 8, S-753 10 Uppsala, Sweden. 3. ____ Transfer to bank account: Foereningsbanken Uppsala, No. 7124-12-773-70, Box 276, S-753 22 Uppsala, Sweden. 4. ____ Credit Card: ____ American Express ____ Visa ____ Master Card ____ Eurocard Number:____________________ Exp. Date:____ Signature:___________________ Card Holder: ___________________________________________________________ Authorized address of card holder: _____________________________________ ACCOMMODATION ____ I will make my own arrangements. Please number your accommodation reservation in order of preference! Arrival date:__________ Departure date:__________ Hotels Single Room Double Room Hotel Svava ____ 675 SEK ____ 800 SEK Hotel Linne ____ 650 SEK ____ 850 SEK Samarithemmets G{sthem ____ 430 SEK ____ 650 SEK (shower in corridor) (shower in corridor) Tariffs quoted are per room per night including breakfast and all rooms have private WC and shower/bath, if not otherwise specified. Prices are subject to adjustment Single Room Double Room Accommodation ____ 190 SEK/1st night ____ 190 SEK/1st night in private rooms (price per person) ____ 150 SEK/2nd night ____ 150 SEK/2nd night ____ 3-Bed-room; 150 SEK/night Sheets for hire; 35 SEK. Breakfast is not included. Access to kitchen. I'm sharing my double/triple room with: _____________________________________ o Hotel reservations will be handled on a ``first come - first served'' basis. o Payment for the hotel can be made in cash or by credit card when leaving the hotel. USEFUL INFORMATION o All fees, except an administration cost of SEK 400 will be refunded, if cancellations are made before August 1, 1994. No refunds will be given after August 1, 1994. o The confirmation will be sent out in July 1994. Return this form BEFORE JULY 15, 1994 to: Uppsala Turist & Kongress ``CONCUR-94'', Fyris torg 8, S-753 10 Uppsala, SWEDEN. Tel: +46-18-27 48 07. Fax: +46-18-69 24 77. ------------------------------------------------------------------------------ Message 3; Postmarked Tue Jun 28 05:49:49 1994 From: JUK@vtttko.tko.vtt.fi (Jukka Karjalainen VTT Electronics, tel +358 81 55 12 401, fax +358 81 55 12 320, e-mail jukka.karjalainen@vtt.fi) Subject: Cfp: Euromicro workshop on Real-time Systems 1995 7TH EUROMICRO WORKSHOP ON REAL-TIME SYSTEMS Odense, Denmark June 14-16, 1995 REFERENCE ADDRESSES Program Chairman Lorenzo Mezzalira Politecnico di Milano Dip. Elettronica e Informazione Piazza Leonardo da Vinci 32 I-20133 Milano, Italy tel. +39-2-2399-3633 fax +39-2-2399-3411 e-mail mezzalir@ipmel2.elet.polimi.it Deputy Program Chairman Angelo Morzenti Politecnico di Milano Dip. Elettronica e Informazione Piazza Leonardo da Vinci 32 I-20133 Milano, Italy tel. +39-2-2399-3634 fax +39-2-2399-3411 e-mail morzenti@ipmel2.elet.polimi.it Organizing Chairman Benny Graff Mortensen The Institute of Applied Computer Science IFAD-Forskerparken 10 DK-5230 Odense M, Denmark tel. + 45 65 93 23 00 fax +45 65 93 2999 e-mail benny@ifad.dk Deputy Organizing Chairman Rene Elmstroem The Institute of Applied Computer Science IFAD-Forskerparken 10 DK-5230 Odense M, Denmark tel. + 45 65 93 23 00 fax +45 65 93 2999 e-mail rene@ifad.dk EUROMICRO PO BOX 2346 NL - 7301 EA Apeldoorn, The Netherlands Tel. + 31 55 55 73 72 Fax + 31 55 55 73 93 e-mail: euromicro@info.vub.ac.be IMPORTANT DATES Submission of extended summaries or proposals: November 15th 1994 Notification of acceptance February 6th 1995 Camera-ready full papers due March 15th 1995 MORE INFORMATION More information on the Workshop and the final Program can be requested to the Euromicro Office or to the Program Chairman. ------------------------------------------ CALL FOR PAPERS The seventh Euromicro Workshop on Real- time Systems is a forum aimed at covering state-of-the-art research and development in real time computing, which is more and more emerging as an essential discipline in the field of computer science and engineering. Topics of interest include, but are not limited to (RTS = Real-Time Systems): RTS SPECIFICATION AND DESIGN: - Behavior specification / description formalisms - Design and verification methodologies - Performance evaluation and verification - Concurrent engineering. RTS HARDWARE: - Architectures and distributed systems - Real-time oriented devices / coprocessors - Timing engines. RTS SOFTWARE: - Architectures and distributed systems- Languages - Operating systems - Scheduling - Debugging - Software reuse. RTS APPLICATIONS: - Embedded systems for automation, sensors /actuators - Knowledge-based systems - Digital Signal Processing - Animation and simulation. RTS RELATED TOPICS: - Communications and Fieldbuses - Fuzzy systems - Object- oriented approaches - HW/SW codesign - Fault-tolerance techniques - Quality of Service SUBMISSION OF PAPERS Prospective authors are encouraged to send five copies of an extended summary not exceeding five pages, clearly showing the name, mailing address, the e-mail address and fax number of the author to contact. The task of the referees will be made easier if a brief statement is added pointing out the aspects of the paper which are yet unpublished and of special value to the Real Time area. A reference is also suggested to the framework proposed in the back of this page. The following declaration should be added: All necessary clearances for the publication of this paper have been obtained. If accepted, the author will prepare the final manuscript in time for inclusion in the proceedings and will personally present the paper at the workshop. The closing date for submissions is November 15th 1994. Authors will be notified of acceptance by February 6th 1995. Camera-ready versions of the full papers in 6 pages IEEE format will be required by March 15th 1995. The proceedings will be published by IEEE Computer Society. SPECIAL SESSIONS Proposals of special sessions or panels are welcome. Please send suggestions to the program chairman before the submissions deadline. GENERAL INFORMATION The workshop will be arranged in The International Science Park of Odense, situated only 10 minutes from the town centre. Odense is in the Funen Island, a beautiful place during summertime. Hans Christian Andersen, the world-famous writer of fairy-tales, spoke glowingly of Funen. He called it "the Garden of Denmark". Funen and its surrounding islands give you the whole Denmark in concentrated form. Splendid scenery, quaint towns containing buildings of old- world charm, safe bathing beaches, ideal conditions for sailing and wind-surfing, history and culture. ------------------------------------------ A Framework for RT-Systems Real-Time Systems designers strongly need a global framework encompassing the different levels/phases of the application realizations in an integrated collection of concepts, formalisms, methodologies, tools, techniques and devices. A synthetic reference can be layered as follows: Requirements Architecture Implementation Technology Requirements: definition of states and their constraints in time and space. Architecture: modeling of computing agents and their interactions. Implementation: operating systems, algorithms and devices. In order to clarify how contributions relate to an application perspective, authors are invited to introduce their works with a brief reference to the proposed framework, possibly answering questions as: * What level is their contribution dealing with, * What kind of analysis is required at an upper level, * What kind of simulation can be used to validate their approach upward, * How a lower level is synthesized. Some examples Occam programs define an architecture. They require an analysis in order to have a distributed state space. Validation is through prototyping with simulated multiprocessing. Synthesis is through placement on processors and links. Scheduling algorithms define an implementation. They require an architecture consisting of a set of processes with given time demands. They give a priority scheme to be used in a kernel or in specialized hardware for a multiprogrammed solution. ------------------------------------------------------------------------------ Message 4; Postmarked Tue Jul 5 09:28:19 1994 From: lwelch%gollum@relay.nswc.navy.mil (Lonnie Welch) Subject: 3rd Workshop on Parallel and Distributed Real-Time Systems +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ CALL FOR PAPERS JOINT WORKSHOP ON PARALLEL AND DISTRIBUTED REAL-TIME SYSTEMS (3rd Workshop on Parallel and Distributed Real-Time Systems and 7th International Real-Time Ada Issues Workshop) April 24-26, 1995 Santa Barbara, California Program Co-Chairs: Theodore Baker, Florida State Univ. (Ada and Ada 9X) Dieter K. Hammer, Eindhoven Univ. of Technology (Europe and Africa) Yoshiaki Kakuda, Osaka University, (The Pacific Rim) Lonnie R. Welch, New Jersey Inst. of Technology (The Americas) Program Committee: John Barnes, UK Maarten Boasson, Hollands Signaal, The Netherlands Alan Burns, University of York, U.K. Steve Case, Computing Devices Int., USA Klaus Ecker, Technical University of Clausthal, Germany Loe Feijs, Philips Research, The Netherlands Borko Furht, Florida Atlantic University, USA Anthony Gargaro, Computer Sciences Corporation, USA Michael Gonzalez, Spain John Goodenough, Software Engineering Institute Robert Harrison, Naval Surface Warfare Center, USA Guenter Hommel, Technical University of Berlin, Germany Keith Hopper, New Zealand Mathai Joseph, University of Warwick, U.K. Joerg Kaiser, GMD, Germany Mike Kamrad, Computing Devices Int., USA Jan van Katwijk, Delft University of Technology, The Netherlands Jyh C. Liu, Texas A&M University, USA Jane W. S. Liu, University of Illinois, USA Douglass Locke, Loral Federal Systems Division, USA Mike Rodd, University of Wales, U.K. Kang G. Shin, University of Michigan, USA Behrooz Shirazi, University of Texas, USA Sang Son, University of Virginia, USA John A. Stankovic, University of Massachusetts, USA Robert Steigerwald, U. S. Air Force Academy, USA Alfred Strohmeier, Swiss Fed Inst of Technology, Switzerland Kenji Toda, MITI Electrotechnical Lab., Japan Morikazu Takegaki, Mitsubishi Electric Company, Japan Joyce Tokar, Tartan Laboratories, USA Richard Volz, Texas A&M University, USA Andrew Wellings, University of York Mark Wilson, Naval Surface Warfare Center, USA Tomohiro Yoneda, Tokyo Institute of Technology, Japan Wei Zhao, Texas A&M University, USA Real-time systems frequently employ parallel and distributed computer platforms in order to meet timing constraints and to achieve fault tolerance and availability. In order to come to a usable solution, the issues of concurrency and dependability must be considered simultaneously. However, it is often the case that researchers focus on problems relevant to concurrent processing while overlooking timeliness. Similarly, real-time computing research efforts are often focused on producing techniques that apply only to single processor systems. To address this unfortunate state of affairs, the 3rd Workshop on Parallel and Distributed Real-Time Systems (WPDRTS3) will be held April 24-26, 1995, in conjunction with the The 9th IEEE International Parallel Processing Symposium (IPPS). Furthermore, in an effort to focus on problems of importance to those who are building concurrent real-time systems in Ada, WPDRTS3 will be held jointly with the 7th International Real-Time Ada Issues Workshop. Thus, in addition to considering issues relevant to concurrent real-time systems in general, the workshop will also focus on issues pertinent to concurrent, real-time Ada and Ada 9X. A partial list of topics of interest include: -Architecture, hardware, communication systems and protocols -Operating systems -Hard and soft real-time systems -Scheduling, resource allocation, and optimization -Programming languages and compiler techniques -Complex systems engineering and reengineering -Object-based techniques -Design and requirements -Applications (including multimedia, databases, artificial intelligence, command and control, and transportation) -Comparison of Ada/Ada 9X with other languages for real-time programming -Implementation/performance of Ada/Ada 9X real-time and concurrent features and Annexes -Advances in real-time Ada/Ada 9X runtime systems -Using Ada/Ada 9X for real-time concurrent computing To submit a manuscript for presentation at the workshop, send a copy by electronic mail (either in PostScript or ASCII format), or send three copies by surface mail, by Oct. 1, 1994 to the appropriate program co-chair. Manuscripts pertaining to Ada or to Ada 9X should be submitted to T. Baker. All other submissions should be sent to the program chair located in your geographic region. Manuscripts should not exceed 2500 words (about 10 pages). The format of the workshop will be a mixture of paper presentations, panel discussions, and problem-solving discussions. In addition to the workshop proceedings, a special issue of The ISMM International Journal of Mini and Microcomputers is planned, in which selected papers from the workshop will be published. Program Co-Chair (for Ada-related papers): Theodore Baker Florida State University Internet: baker@cs.fsu.edu Program Co-Chair (for Europe and Africa) Dieter K. Hammer Dept. of Mathematics and Computing Science Eindhoven Univ. of Technology P. O. Box 513 NL-5600 MB Eindhoven The Netherlands +31 40 474416 Internet: hammer@win.tue.nl Program Co-Chair (for the Pacific Rim) Yoshiaki Kakuda Dept. of Information and Computer Sciences Faculty of Engineering Science Osaka University 1-3, Machikaneyama-cho, Toyonaka-shi Osaka 560, Japan +81 6 844 1151 ext.4841 Internet: kakuda@ics.es.osaka-u.ac.jp Program Co-Chair (for The Americas) Lonnie R. Welch Dept. of Computer and Information Science New Jersey Institute of Technology University Heights Newark, NJ 07102 (201) 596-5683 Internet: welch@vienna.njit.edu IPPS is sponsored by The IEEE Computer Society Technical Committee on Parallel Processing in cooperation with ACM SIGARCH. The joint workshop on is sponsored by The U.S. Naval Surface Warfare Center, and is held in cooperation with The IEEE Computer Society Technical Committee on Parallel Processing, and with The IEEE Computer Society Technical Committee on Real-Time Systems. Cooperation with ACM SIGAda is also pending. ------------------------------------------------------------------------------ Message 5; Postmarked Tue Jul 12 22:13:08 1994 From: son@bbibbi.cs.virginia.edu Subject: ISMM Conference on Intelligent Information Management Systems Call For Papers ISMM International Conference on Intelligent Information Management Systems June 7-9, 1995 Washington D.C. SPONSORED by The International Society for Mini and Microcomputers- ISMM Technical Committee on Information Management Systems Authors are invited to submit original papers in all aspects of information management systems and intelligent systems including, but not limited to, the following subject categories: 1 Database Management Systems 2 Object-Oriented Database 3 Multidatabases 4 Distributed Computing Environment 5 Client-Server Systems 6 Networking & Communication Protocols 7 Intelligent Information Management Systems 8 Expert Systems 9 Knowledge-Based Systems 10 Multimedia Systems 11 Hypertext and Hypermedia Systems 12 Real-Time Systems 13 Information Technology SUBMISSION OF PAPERS Five copies of the original research papers (maximum of 15 double-spaced pages using point size of 12) should be received by the program chair, Prof. J. Wong, Dept. of Computer Science, Iowa State University, Ames, Iowa 50011, USA, by October 15, 1994. A cover page should contain the title, authors names, affiliation, address, Fax number, e-mail address, an abstract and three keywords (taken from the list of conference topics). Fax or e-mail submissions will not be considered. A letter must be included confirming that at least one of the authors will register and attend the conference if the paper is accepted. Notification will be mailed by February 15, 1995. The final camera ready manuscripts are due April 1, 1995 for publication in the proceedings. Electronic submission of the final manuscript in postscript format is encouraged. Authors wishing to have their papers considered for possible publication in either the ISMM International Journal of Mini and Microcomputers or the ISMM Journal of Microcomputer Applications should send three copies of the expanded paper directly to the Editors of the respective journals. General Chair Program Chair Local Arrangements Chair Prof. S. Pakzad Prof. J. Wong Prof. M. Owrang Dept. of EE, 121, EE East Dept. of Computer Sci. Dept. of Computer Sci. Pennsylvania State University Iowa State University The American University University Park, PA 16803, USA. Ames, Iowa 50011, USA. Washington D.C. 20016, USA. Tel:(814) 863-1265 Tel:(515) 294-2586 Tel:(202) 885-3159 Fax:(814) 865-3176 Fax:(515) 294-0258 Fax:(202) 885-2013 Program Committee: M. Bright, University of Pittsburgh C. Egyhazy, Virginia Polytechnic Institute & State University B. Furht, Florida Atlantic University M. Eich, Southern Methodist University M. Frame, Institute for Defense Analysis J. Ho, Columbus College A.R. Hurson, Pennsylvania State University B. Jin, Christopher Newport University D. Jungmann, University of Desden, Germany M. Mizuno, Kansas State University L. Miller, Iowa State University S. Kiaei, Motorola R. Korfhage, University of Pittsburgh J. Leszczylowski, Polish Academy of Science B. Shirazi, University of Texas at Arlington S. Son, University of Virginia W. Subbarao, Florida International University D. Tavangarian, Fern Universitat Hagen, Germany B. Thuraisingham, Mitre Corporation L. Ye, Huazhong University of Science and Technology, China C.H. Yen, Ball State University ------------------------------------------------------------------------------ <<<<<<<<<<<<<<<<<<<* 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 ------------------------------------------------------------------------------