A talk by Elizabeth Leonard
5PM, December 4th, 1997. Shaffer 3.
This talk will introduce the basic concepts of process algebras and show how they can be used to reason about the behavior of real-time and object-oriented systems.
A process can be thought of as a program or machine which performs both observable and invisible actions and also interacts with its environment. This environment may include a human user as well as other concurrently operating processes. Process algebras are one of the formalisms which have been used to describe the behavior of processes. Numerous equivalences have been developed to relate processes based on their observable behavior. We will focus mostly on the testing preorders, which relate processes based on the set of "tests" that the processes may and must pass, with tests generally thought of as processes for which there is a designated success action.
The general process algebra framework will be extended to allow us to reason about the time dependent behavior of processes. Time dependent behavior includes delays, upper and lower bounds on delays, and time-outs. This type of behavior is sensitive to the internal computation of the process. We will introduce a timed testing theory for general real-time systems as well as for a class of timed systems for which the preorders capture a notion of "faster than".
Finally, we will show how a process algebra can be used to reason about the message-passing behavior of an object-oriented system. A translation from POOL (Parallel Object-Oriented Language) to an object-oriented variant of process algebra will be presented. Another equivalence, trace equivalence, will be used to show that two programs in POOL are equivalent if and only if their translations are equivalent. Trace equivalence relates processes based on the sequence of actions that they can perform. The relationship between traces and testing theory will be shown.