Translating testing theories for concurrent systems

Abstract

In this article the “classical” topic of theory translation is revisited. It is argued that the importance of this research field is currently growing fast, due to the necessity of re-using known theoretical results in the context of novel semantic frameworks. As a practical background, we consider cyber-physical systems and their development and verification in distributed collaborative environments, where multiple modelling formalisms are used for different sub-systems. For verification of the integrated system, these different views need to be integrated and consolidated as well, in order to ensure that the required emergent properties have been realised as intended. The topic is illustrated by a practical problem from the field of runtime verification. It is shown how a class of complete health monitors (i.e. checkers monitoring system behaviour) elaborated within the semantic framework of Kripke structures and LTL assertions can be re-used for runtime verification in the context of the CSP process algebra with trace/refusal specifications. We point out how crucial ideas for this theory translation have already been anticipated in Ernst-Rüdiger Olderog’s early work.