Describing a signal analyzer in the process algebra PMC -- A case study

H. R. Andersen, M. Mendler

In this paper we take a look at real-time systems from an implementation-oriented perspective. We are interested in the formal description of genuinely distributed systems whose correct functional behaviour depends on real-time constraints. The question of how to combine real-time with distributed processing in a clean and satisfactory way is the object of our investigation. The approach we wish to advance is based on PMC, an asynchronous process algebra with multiple clocks. The keywords here are `asynchrony' as the essential feature of distributed computation and the notion of a `clock' as an elementary real-time mechanism. We base the discussion on an actual industrial product: The B&K 2145 Vehicle Signal Analyzer, an instrument for measuring and analyzing noise generated by cars and other machines with rotating objects. We present an extension of PMC by ML-style value passing and demonstrate its use on a simplified version of the B&K Signal Analyzer.