Process algebra semantics of phiSDL

Abstract

A new semantics of an interesting subset of the specification language SDL is given by a translation to a discrete-time variant of process algebra in the form of ACP extended with data as in muCRL. The strength of the chosen subset, called phiSDL, is its close connection with full SDL, despite its dramatically reduced size. Thus, we are able to concentrate on solving the basic semantic issues without being in danger of having to turn the results inside out in order to deal with full SDL. Novel to the presented semantics is that it relates the time used with timer setting to the time involved in waiting for signals and delay of signals.

Preprint available here.