: Semantics of description languages for complex systems are a central issue for implementing verification methods such as abstract model checking . This technique is employed to verify systems by inspecting only a small state space that represents its potential behaviors. This paper presents a generalized operational semantics of the modelling language promela that provides the theoretical basis to introduce this promising method in the model checker SPIN. The generalization consists of identifying language aspects affected by the abstraction. Using these aspects as parameters, it is possible to obtain and relate different interpretations of the language. The new semantics provides a framework to reason about how to construct the tool αspin as an extension of spin.

The aim of IEEE Time-Sensitive Networking (TSN) standards is to grant deterministic communication in traditional Ethernet networks for Industry 4.0. Insofar as the use cases in the Factory need some mobility, the extension of the TSN capabilities over the fifth-generation (5G) cellular network is the next step. Some challenges in TSN over 5G, such as TSN translators time synchronization functionality, are well defined in the standards, even if they have not yet been addressed in the market. However other challenges, such as the dynamic configuration of the entire network (or part of the it) based on quality requirements of the current TSN traffic pattern, are defined at a very high level and delegated to vendors for implementation. This paper addresses this challenge, using an Automata Learning approach to monitor and reconfigure the end-to-end 5G QoS flow to keep the quality of a TSN session within the required values. Additionally, algorithms are provided to build the automata from network data and predict potential deviations of the requirements to meet the expected quality. Moreover, this work presents a functional TSN over a 5G testbed where the algorithms have been tested, demonstrating that the proposed solution achieves an improvement of around 40% compared to the usual operation of the network.