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
------------------------------------------------------------------------------