Revisiting Semantics of Interactions for Trace Validity Analysis

TL;DR

This paper introduces an operational method for analyzing the semantics of interaction languages like MSC, focusing on immediate actions and trace validity, supported by algorithms and experimental evaluation.

Contribution

It proposes a novel operational approach to semantics of interaction languages, differing from traditional translation methods, with algorithms for semantic computation and trace validation.

Findings

Algorithms effectively compute semantics and validate traces.

Experimental results demonstrate the approach's practicality.

Operational semantics offer a new perspective on interaction analysis.

Abstract

Interaction languages such as MSC are often associated with formal semantics by means of translations into distinct behavioral formalisms such as automatas or Petri nets. In contrast to translational approaches we propose an operational approach. Its principle is to identify which elementary communication actions can be immediately executed, and then to compute, for every such action, a new interaction representing the possible continuations to its execution. We also define an algorithm for checking the validity of execution traces (i.e. whether or not they belong to an interaction's semantics). Algorithms for semantic computation and trace validity are analyzed by means of experiments.