Technical interoperability is the first and foremost requirement for the Industrial Internet of Things. It ensures connectivity and networking between heterogeneous devices and systems, enabling their collaboration across different network protocols, both locally and over the Internet. Devices designed for industrial use are well known for their robustness, precision, and high-quality finish; however, they typically come with one or a few fixed industrial network protocols. One traditional method of connecting two devices using different protocols is to use a converter that translates messages between the two network interfaces. This paper proposes a unified protocol translation method for multiple network interfaces. The method is validated in a product assembly line use case, in which the involved devices use four different industrial Ethernet protocols and frameworks: Modbus TCP, EtherNet/IP Class 1, OPC UA PubSub, and ROS 2. Moreover, the correctness of such a complex networking system is verified using a runtime verification approach grounded in a formal interaction model, ensuring that the observed communication behaviors conform to the expected specification.

This paper presents an approach leveraging symbolic execution techniques to generate test cases from models mixing data and time. Our methodology focuses on symbolic paths, satisfying a trace-determinism property, which allows testing behaviors in the presence of uninitialized state variables. We construct tree-like test cases around these test purposes, with verdicts on their leaves, meticulously crafting verdict conditions from symbolic execution path conditions encoding temporal data-dependent constraints. Our test case generation is implemented within the symbolic execution platform Diversity. Through experiments, we provide metrics and quantify some aspects of the generated test cases, including the reachability of verdicts within observation time frames specified by the tester.

Cyber-Physical Systems (CPS) contain complex computational components that control physical entities.The design of these components must take into account the realtime and concurrent nature of these systems.Formulating requirements that describe CPS behaviors precisely, ruling out misunderstandings, is a crucial yet difficult endeavor.To increase trust in the requirements, formal methods can be used to check relevant properties of the requirements.We investigate a process algebra to capture real-time behaviors and concurrency in CPS requirements in order to automate their analysis.We use a structured natural language to first express CPS requirements: this takes into account current practice, indeed requirements should be easily writable as well as graspable by stakeholders with various points of view and ease communication among them.At the same time, requirements analysis using simulation or formal validation is possible by taking advantage of the requirements structure.We discuss translation from the structured requirements into the process algebra to automate the overall process.Our approach is implemented and is illustrated by an example issued from CPS4EU project 1 .

Data flow formalisms are commonly used to model systems in order to solve problems of buffer sizing and task scheduling. A prerequisite for static analysis of a modeled system is the existence of a periodic schedule in which the sizes of communication channels can be bounded for an unbounded execution (consistency), and that communication dependencies do not introduce a deadlock in such an execution (liveness). In the context of Cyber-Physical Systems, components are often interfaced with the physical world and have frequency constraints. The existing data flow formalisms lack expressiveness to fully cover the expected behavior of these components. We propose an extension to Synchronous Data Flow (SDF) formalism, called Polygraph, that includes frequency constraints and adjustable communication rates. We show that with these extensions, the conditions for a model to be consistent and live are no longer sufficient, and we extend the corresponding theorems with necessary and sufficient conditions to preserve these properties. We also introduce a framework to check the liveness of a Polygraph model, implemented in the tool DIVERSITY, along with preliminary experiments to validate this approach.

Modern industrial systems are often large and distributed. Consequently, building the test harness for them can be technically challenging. A compositional approach attempts to overcome this problem by partitioning the system into smaller parts easier to test separately. And in particular, compositionality helps to avoid as much as possible testing the whole monolithic system thanks to mathematical results which relate the global correctness of the system to the correctness of its constituent parts. In this paper, we present a compositionality result for model-based testing in the setting of the conformance relation tioco which is dedicated to timed systems. We show how to exploit this result in practice by extending a previously defined symbolic testing framework.

This paper presents a symbolic execution framework devoted to system models, recursively defined by interconnecting component models. Our concern is to allow one to explicitly define interaction rules between components, while taking into account those rules at the symbolic execution phase. The paper introduces a small set of primitives dedicated to this purpose, together with their associated symbolic execution rules.

Slicing communicating automata specifications is a model reduction technique that has been shown to be efficient in our previous works. This paper introduces Carver, a tool for slicing communicating automata specifications, that underlies dependence-based slicing techniques. It is described how this tool can extract slices from specifications, and how it can be integrated in the environment of other tools, for the purpose of reducing the complexity of formal analyses.