Subject: IEEE-RTTC digest for Wed Jul 15, 1992 ------------------------------------------------------------------------------ ##### ##### ##### ##### #### ##### ##### ### # # # # # # # # # # # # # # # # # # # # #### #### #### #### #### # # # # # # # # # # # # # # # # # # # # # # ##### ##### ##### ##### # # # # ### ------------------------------------------------------------------------------ The Electronic Newsletter of the IEEE Technical Committee on Real-Time Systems ------------------------------------------------------------------------------ Table of Contents Line ----------------- ---- 1. sas@sbcs.sunysb.edu (468 lines) Post doc announcement.............................................. 2 CONCUR '92 --- abstracts of invited talks & tutorials.............. 32 ------------------------------------------------------------------------------ <<<<<<<<<<<<<<<<<<<<* START OF THE IEEE-RTTC NEWSLETTER *>>>>>>>>>>>>>>>>>>>>> ------------------------------------------------------------------------------ Message 1; Postmarked Mon Jun 29 22:33:41 1992 Subject: Post doc announcement From: rance@science.csc.ncsu.edu (Rance Cleaveland) POSTDOCTORAL RESEARCH POSITION I am seeking to fill a research position in the Computer Science Deparment at North Carolina State University. The project involves the development of tools and theories for verifying concurrent finite-state systems and is supported by a grant from the U.S. National Science Foundation. The successful applicant will possess a PhD (or equivalent) and will be knowledgeable in several of the following: process algebras, formal models of real time, model checking, partial order models of concurrency, verification algorithms, applications of formal methods in system design. Pay will be in the neighborhood of $35,000 per annum, depending on qualifications. Interested parties should send their curricula vitae to: Prof. Rance Cleaveland Department of Computer Science North Carolina State University Raleigh, NC 27695-8206 USA Postmarked Mon Jul 6 13:41:18 1992 Subject: CONCUR '92 --- abstracts of invited talks & tutorials From: sas@sbcs.sunysb.edu Date: Thu, 2 Jul 92 12:01:02 EDT Below, please find the abstracts of the inivted talks and tutorials to be given at CONCUR '92, Third Int'l Conf. on Concurrency Theory, 24-27 Aug. 1992, Stony Brook, NY. A LaTex file of the final program and Call for Registration is available via anonymous ftp from sbcs.sunysb.edu (130.245.1.15). The file is located in pub/CONCUR92/cfr.tex.Z and is in compressed format. ---------- ABSTRACTS OF INVITED TALKS CONCUR '92 .----------------------------------------------------------------------------. | | | Discrete Time Process Algebra | | | | Jos Baeten | | Eindhoven University of Technology | | | | Process Algebra in the form of ACP, CCS or CSP describes the main features | | of imperative concurrent programming without any explicit mention of | | time. Implicitly, time is present in the interpretation of sequential | | composition, in that the first of a sequenced pair of processes must be | | executed before the second. It may be felt as a weakness that time only | | features implicitly. Indeed a quantitative view on the relationship | | between process execution and progress of time is definitely absent in | | these calculi. This seems worse than it actually is. Nothing prevents | | one to introduce timer processes that represent clocks, to have processes | | interacting with these clocks and to have synchronisations between the | | clocks in ACP, CCS or CSP. | | | | Of course timing aspects can be described more uniformly if process | | algebras are given that provide standardised features to incorporate a | | quantitative view on time. Obvious as this may seem, the more obvious | | observation is that in a few years so many different formats for timed | | process algebras have been introduced that this uniformity seems to be | | further away than before. There are several reasons for the emerging | | spectrum of timed process algebras. This can be explained by considering | | various options for adding time. The most obvious option is to represent | | time by means of non-negative reals, and to have time stamps on actions. | | | | Another options is to divide time in slices indexed by natural numbers, to | | have a time stamping mechanism that provides each action with the time | | slice in which it occurs and to have a time order within each slice only. | | This has been worked out in ATP, a process algebra that adds time slicing | | to aprACP, a version of ACP based on action prefixing rather than | | sequential composition. | | | | In this talk we extend ACP to a discrete time process algebra. This is | | done by adding a new process constructor which represents the delay of a | | process for one time unit. For practical applications, we include further | | the key operators of ATP, namely unit delay and maximal progress | | composition. We design our discrete time process algebra in an | | incremental way, and motivate our choices with each increment of the | | algebra and compare it with other developments of discrete time process | | algebra. | | | `----------------------------------------------------------------------------' .----------------------------------------------------------------------------. | | | At-Most-Once Message Delivery: | | A Case Study in Algorithm Verification | | | | Nancy Lynch | | MIT | | | | The at-most-once message delivery problem involves delivering a sequence | | of messages submitted by a user at one location to another user at another | | location. If no failures occur, all messages should be delivered in the | | order in which they are submitted, each exactly once. If failures (in | | particular, node crashes, lost messages or timing anomalies) occur, some | | messages might be lost, but the remaining messages should not be reordered | | or duplicated. | | | | This talk examines two of the best-known algorithms for solving this | | problem: the clock-based protocol of [LSW] and the five-packet interchange | | protocol of [B]] It is shown that both of these protocols can be | | understood as implementations of a common (untimed) protocol that we call | | the generic protocol. It is also shown that the generic protocol meets | | the problem specification. | | | | The development is carried out in the context of (timed and untimed) | | automata [LV], [LT], using simulation techniques [LV]. It exercises many | | aspects of the relevant theory, including timed and untimed automata, | | refinement mappings, forward and backward simulations, history and | | prophecy variables. The theory provides insight into the algorithms, and | | vice versa. | | | | This talk represents joint work with Butler Lampson and Jorgen | | Sogaard-Andersen. | | | | [LSW] Barbara Liskov, Luiba Shrira and John Wroclawski, "Efficient | | At-Most-Once Messages Based on Synchronized Clocks." | | MIT/LCS/TR-476, April, 1990, Laboratory for Computer Science, | | Massachusetts Institute of Technology, Cambridge, MA 02139. | | | | [B] Dag Belsnes, "Single Message Communication." IEEE | | Transactions on Communications, Vol. Com-24, No. 2, February, | | 1976. | | | | [LV] Nancy Lynch and Frits Vaandrager, "Forward and Backward | | Simulations for Timing-Based Systems." In Proceedings of REX | | Workshop "Real-Time: Theory in Practice," Springer-Verlag, | | LNCS 600, 1992, Mook, The Netherland. | | | | [LT] Lynch, N. and Tuttle, M. "An Introduction to Input/Output | | Automata," CWI-Quarterly, No. 3, Vol. 2, September, 1989, | | pages 219-246. | | | `----------------------------------------------------------------------------' .----------------------------------------------------------------------------. | | | The Polyadic pi Calculus | | | | Robin Milner | | University of Edinburgh | | | | The pi calculus is a calculus of concurrent processes based upon the idea | | of naming. It models dynamically changing concurrent systems, has a rich | | algebraic theory, and contains in a precise way both functions (the lambda | | calculus) and data structures, represented as processes. The calculus is | | a generalization of CCS, and was introduced by Robin Milner, Joachim | | Parrow and David Walker, based on important ideas of Mogens Nielsen and | | Uffe Engberg. | | | | The way in which everything is built upon naming is this: When two | | processes interact, they use a name (which can be thought of as a | | channel). This name is called the subject of the interaction. The object | | of an interaction (its information content) is also a name; this is the | | mention of a name, not the use of it. To receive a name is to acquire the | | ability to use it, perhaps to interact with a process which was previously | | inaccessible. This process may indeed represent a datum, as explained | | above; then one can think of the datum itself having been received. | | | | In this lecture I shall discuss the polyadic version of the pi calculus, | | which supports a very fruitful notion of sort and sorting, akin to simple | | typing in the lambda calculus. It will be seen how different sortings are | | appropriate for different applications. The encoding of the lambda | | calculus into pi calculus, and the uniform representation of data | | structures, are best seen in the polyadic setting with suitable sortings. | | | `----------------------------------------------------------------------------' .----------------------------------------------------------------------------. | | | How Vital is Liveness? | | Proving Timing Properties of Hybrid and Reactive Systems | | | | Amir Pneuli | | Weizmann Institute of Science | | | | We propose a framework for the formal specification and verification of | | timed and hybrid systems. For timed systems we propose a specification | | language that refers to time only through age functions which measure the | | length of the most recent time interval in which a given formula has been | | continuously true. | | | | We then consider hybrid systems, which are systems consisting of a | | nontrivial mixture of discrete and continuous components, such as a | | digital controller that controls a continuous environment. The proposed | | framework extends the temporal logic approach which has proven useful for | | the formal analysis of discrete systems such as reactive programs. The | | new framework consists of a semantic model for hybrid time, the notion of | | phase transition systems, which extends the formalism of discrete | | transition systems, an extended version of Statecharts for the | | specification of hybrid behaviours, and an extended version of temporal | | logic that enables reasoning about continuous change. | | | | The talk is based on extensive collaboration with Z. Manna, T. Henzinger, | | O. Maller and Y. Kesten. | | | | | `----------------------------------------------------------------------------' .----------------------------------------------------------------------------. | | | The Duality of Time and Information | | | | Vaughan Pratt | | Stanford University | | | | The states of a computing system bear information and change time, while | | its events bear time and change information. We develop a primitive | | algebraic model of this duality of time and information for straightline | | code in the absence of nondeterminism and concurrency, where time and | | information are linearly ordered, demonstrating that this natural duality | | of computation is more fundamental than the natural logic of computation | | in which nondeterminism is disjunction and concurrency conjunction. | | | | To accommodate distributed computing systems we then bring in these two | | logical connectives, in the process passing to partially ordered time and | | information. Some flexibility in how this is done permits a perfectly | | symmetric logic of computation. The natural form taken by this logic is | | essentially full linear logic, showing that linear logic arises | | automatically as a logic of full computation, namely computation attaching | | equal importance to nondeterminism and concurrency. | | | | We conclude with an assessment of the prospects for extending the duality | | to other organizations of time and information besides partial orders in | | order to accommodate real time, nonmonotonic logic, and automata that can | | forget. | | | `----------------------------------------------------------------------------' ABSTRACTS OF TUTORIALS CONCUR '92 .----------------------------------------------------------------------------. | | | Finite-State Models of Real-time Behavior | | | | Rajeev Alur David L. Dill | | AT&T Bell Laboratories Stanford University | | | | Finite-state models of various kinds have been very useful for automatic | | formal verification of concurrent systems. Many verification algorithms | | have been developed for both branching-time and linear-time models, and | | the methods have been applied successfully to non-trivial systems. | | | | However, there is now a great deal of interest in modelling and formal | | verification of real-time concurrent systems, for which quantitative | | delays are crucial to "correct" behavior. It is not too difficult to | | incorporate timing constraints into ordinary finite automata if time is | | considered to be discrete. However, time is often regarded as a | | continuous quantity, and continuous time is the most natural model for | | some physical processes. | | | | One method for incorporating continuous time into finite automata is to | | annotate finite-state models with real-valued counters, called clocks, | | which keep track of the delays between events. These tutorial lectures | | will discuss some of the surprises that arise from the study of timed | | finite automata, as well as how they can be applied to the modelling and | | verification of real-time systems. | | | | In the linear-time case, we can consider these automata to accept timed | | strings, which record not only the order of events but their times of | | occurrence. The set of timed strings accepted by a timed automaton can be | | considered to be a timed formal language, which immediately prompts one to | | ask the usual questions about decidability and closure properties. Some | | of the answers are surprising: for nondeterministic automata, emptiness is | | decidable but universality is not (while in the discrete case, both are | | decidable). | | | | In the branching-time case, it is interesting to consider the problem of | | model-checking of formulas in a timed dialect of computation tree logic | | (CTL). There are some surprises here, also: the model-checking problem | | is fully decidable, but the logic itself is not. | | | | We believe that timed automata in various forms will be useful for | | modelling and verifying real-time systems. Furthermore, the results can | | be adapted to other similar problems (for example, checking bisimulation | | in real-time process algebras). There are also numerous questions about | | timed languages and automata that have yet to be answered. | | | `----------------------------------------------------------------------------' .----------------------------------------------------------------------------. | | | Introduction to Process Algebra | | | | Rob van Glabbeek | | Stanford University | | | | This tutorial gives an introduction to and overview of some languages and | | models for representing and reasoning about processes. Attention will be | | restricted to the more classical approaches, omitting recent developments | | on real-time and value passing. | | | | First of all system description languages like CCS, CSP, COSY, ACP and | | MEIJE will be presented and compared. Translations from one language in | | the other will be provided, and the relative expressiveness of the various | | languages will be analyzed. Particular attention will be paid to the | | treatment of nondeterminism, communication between parallel processes, | | recursion, abstraction from internal actions, successful termination, | | deadlock, divergence and underspecification. | | | | The semantics of the languages can be given by means of an interpretation | | in a model of concurrency, or process algebra. This is usually done in two | | steps. In step 1 an interpretation of the language in an underlying model | | (often a particular brand of process graphs, Petri nets or event | | structures) is given. Then in step 2 an equivalence relation on this model | | is divided out in order to abstract from unwanted details in system | | descriptions. Of course this equivalence should be a congruence for all | | language constructs. | | | | Usually step 1 is performed using denotational semantics: an operator is | | associated with every language construct and recursion is dealt with by | | means of fixed point techniques. Alternatively, in case the underlying | | model is based on event structures, the syntactic tree of a process | | expression (or actually the syntactic graph, after eliminating recursion | | operators) can smoothly be transformed in an event structure. In case of a | | transition oriented underlying model (brands of process graphs or Petri | | nets), step 1 can conveniently be performed by means of structured | | operational semantics: the transitions in system representations are | | derived step for step, using a kind of inference mechanism. | | | | If the underlying model is considered abstract enough for a desired | | application, step 2 can be skipped. Such models are called explicit models | | and include the models based on non-well-founded sets or on metric spaces, | | projective limit models and the models in which a process is represented | | by a set of executions (modelled as traces, failure pairs, partial ordered | | multisets, etc.). | | | | Although many different underlying models have been proposed, there exist | | canonical translations between them. Modulo these translations the models | | differ only in size (it can be that a system can be represented in one | | model, but not in another) and in the level of detail of process | | representations (it can be that two systems are represented differently in | | one model, but have the same representation in another one). | | | | Like the underlying models, also the proposed equivalence relations to be | | divided out on these models come in huge quantities. The choice of such | | an equivalence is not without consequences: they are used to determine if | | one system is a correct implementation of another one. Semantic | | equivalences determine or are determined by the relevant properties of | | process representations: two processes are identified iff they have the | | same relevant properties. Of course it is application dependent which | | properties are relevant. Therefore many semantic equivalences coexist. | | | `----------------------------------------------------------------------------' .----------------------------------------------------------------------------. | | | Models for Concurrency | | | | Mogens Nielsen | | Aarhus University | | | | A number of formal models have been suggested and studied in the | | literature as frameworks for understanding the nature of distributed | | computations. Each model has its own set of techniques for expressing and | | reasoning about distributed computational systems. The choice of model for | | a concrete application is often based on a mixture of pragmatic and formal | | considerations. As an aid in this process, these models are often | | classified according to their expressive power, e.g interleaving versus | | noninterleaving, linear time versus branching time, system versus | | behavioural, etc. And recently, these kinds of classifications have been | | supported by theoretical results expressing formal relationships between | | models -- the topic of this talk. | | | | The models and their relationships will be expressed categorically. The | | models will be equipped with a notion of "simulation" morphisms, and the | | relationships will be expressed in terms of certain types of adjunctions | | between our (categories of) models, based on functors viewed as | | translations between individual models. Not only does this give a unified | | presentation of the models (also used in this talk), and formal ways of | | expressing concepts like "one model being more abstract than another"; but | | also it turns out that constructions used in languages like CCS and CSP, | | based on synchronous communication, can be viewed as universal in these | | categories, and hence the semantics may be described in a uniform way for | | many different structures; and in the formal translation between models | | one may use preservation properties of adjoints. | | | | In this tutorial we shall | | | | - give a brief introduction to some fundamental models for concurrency, | | including (Asynchronous) Transition Systems, Petri Nets, | | Synchronization Trees, Event Structures, Hoare Traces and | | Mazurkiewics Traces, and their notions of "simulation" morphisms used | | in this presentation; focussing on the similarities and differences | | of the models with respect to expressive power, based on examples; | | | | - motivate and present the types of results mentioned above; focussing | | on presentation and interpretation of a formal classification of | | models in terms of adjunctions, and also illustrating operational and | | denotational semantics of process algebra in this context; | | | | - present one of the adjunctions -- relationship between Transition | | Systems and Petri Nets -- in some detail; this is one example of an | | important result contributing to the understanding of the distinction | | between so-called interleaving and noninterleaving models. | | | | This talk is based on a chapter "Models for Concurrency" being written | | jointly with Glynn Winskel for the Handbook of Logic in Computer Science | | (Oxford University Press). | | | `----------------------------------------------------------------------------' .----------------------------------------------------------------------------. | | | Efficient Program Transformations for Resilient Parallel Computation | | | | Krishna Palem | | IBM Research Center, Yorktown Heights | | | | With hardware becoming cheaper, it is expected that massively parallel | | systems with large numbers of processors will offer increasingly faster | | computational speeds, at low cost. Unfortunately, these massively | | parallel machines tend to become increasingly fault-prone as well. For | | example, the larger the number of processors, the greater the probability | | of some of them failing. To further compound this problem, much of | | program or algorithm design is typically performed in the context of an | | ideal parallel machine that is unencumbered by failures or other | | imperfections intrinsic to its realistic counterpart. As a consequence, | | these ideal programs are not even guaranteed to run correctly on real | | implementations of parallel machines, whenever the ideal assumptions of | | the programming model are not supported. The aim of this tutorial is to | | describe strategies supporting the resilient (correct) execution of such | | ideal parallel programs on fault-prone parallel machines. | | | | There has been a lot of recent activity in this area, addressing a variety | | of issues. The main concerns of these efforts fall into two categories. | | First, research has been directed towards the design of general strategies | | for deriving resilient computations, that work independent of any | | particular parallel program. Second, these strategies are extremely | | efficient in that the overhead they introduce into the resilient | | computation, relative to the ideal program from which it is derived, is | | provably small. Furthermore, these strategies are fully automatic and can | | be applied as compile-time transformations to the ideal program. | | | | The ideal programming model that we will be considering is that of a | | completely reliable shared-memory parallel machine in which the processors | | can execute in perfect lock-step synchrony, if needed. The canonical | | fault-prone machine on which these programs will actually be executing, is | | one in which the set of resources (including processors) that are assigned | | to the program, fluctuate dynamically during its execution. These | | fluctuations could be induced by phenomena such as failures and repairs, | | or due to rescheduling by the operating system. We will be discussing | | transformations that are applicable in the context of shared memory, as | | well as distributed-memory implementations of these fault-prone parallel | | machines. | | | `----------------------------------------------------------------------------' ------------------------------------------------------------------------------ <<<<<<<<<<<<<<<<<<<<<* END OF THE IEEE-RTTC NEWSLETTER *>>>>>>>>>>>>>>>>>>>>>> ------------------------------------------------------------------------------ The IEEE-RTTC repository is maintained by Azer Bestavros at Boston University Internet address for anonymous FTP to the IEEE-RTTC repository is: cs.bu.edu Contributions to this forum should be sent by E-mail to: IEEE-RTTC@cs.bu.edu Requests or inquiries should be sent by E-mail to: IEEE-RTTC-request@cs.bu.edu ------------------------------------------------------------------------------