Process Algebra versus Axiomatic Specification of a Real-Time Protocol

Abstract

In this paper we present two different approaches used in specifying a well-known audio control protocol with real-time characteristics. The first approach is based on Circal, a process algebra that permits a natural representation of timing properties and the analysis of interesting aspects of timing systems. The second approach is based on the Timed Interval Calculus, a set-theoretical notation for concisely expressing properties of timed intervals. The comparison between the two approaches shows that they are almost complementary: the former allows an easy modelling of the most procedural aspects of the protocol and provides a fully automatic proof but cannot catch all timing aspects; the latter allows easy modelling of all timing properties but the proof is quite hard and cannot be fully automated. This suggests a decomposition of the proof into subproofs to be performed in different proof environments.