Abstract Interaction models describe distributed systems as algebraic terms, with gates marking interaction points between local views. Composing local models into a coherent global one requires aligning these gates while respecting the algebraic laws of interaction operators. This is achieved via anti-unification techniques. We specialize anti-unification (or generalization) via a special constant-preserving variant, which preserves designated constants while generalizing the remaining structure. We develop a dedicated rule-based procedure, for computing these generalizations, prove its termination, soundness, and completeness, extend it modulo equational theories, and integrate it into a standard anti-unification framework. A prototype tool demonstrates the approach’s ability to recompose global interactions from partial views.

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.

We are interested in the safety of critical systems whose development is based on models. Implementing failure analyses for this kind of system requires modeling the failures and conditions of their appearances. The failure analysis approaches are mainly based on the structures of systems where boolean equations depict the propagation of faults. The objective of the analysis is to calculate Minimal Cut Sets (MCS), i.e., the smallest sets of basic faults that may cause a feared event and their probabilities. The most efficient MCS resolution method is based on Binary Decision Diagrams (BDD). In this paper, we present a model-based toolset to construct from SysML structural models of systems, the fault trees, and their BDD-representation enabling us to compute MCS. Faults in our approach are not limited to boolean variables; they can be expressed by constraints coming from an arbitrary decidable theory. We validate the toolset capabilities with an oil burner system use case.

Finding comprehensive and relevant scenarios is a major challenge for autonomous vehicles validation and SOTIF. A functional scenario, e.g. a cut-in, encloses many concrete variations. Formal methods help covering an intermediate level of scenario families, called logical, and capitalizing them in a scenario database. Families are generated from discrete and modular symbolic models through a new subsumption criterion which allows the identification of scenario suffixes which are redundant and eliminate them during the generation. The generation, including the implementation of the subsumption criterion, benefits from: i) the compact representation of models thanks to discretization and symbolic arithmetic, ii) dedicated symbolic execution techniques. Analysis is performed to verify how the generated scenarios cover real situations by confronting them to time series from the modeled system and identify potential gaps in the model. We formally define our approach, implement it in the symbolic execution tool DIVERSITY. Assessment is carried out on a real autopilot black box module from the project 3SA.

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 .

The implementations and testing in real conditions of Autonomous Vehicles (AV) for private usage show important advances. However, a lack still exists in addressing the particularities of AVs for Public Transportation. Such particularities range from limited safety mechanisms aboard, risky situations associated to particular users and complex self-driving situations up to the limited passengers-vehicle interactions possible. Since, to our knowledge, no comprehensive safety assessment actually exists and the current automotive related standards do not address identified aspects, in this paper, we propose to conduct a minimal but representative safety assessment based upon a local but real autonomous vehicle implementation. To conduct our study, the Hazard Analysis and Risks Assessment introduced in the ISO 26262 standard is taken as a basis. Initial outcomes suggest that critical autonomy aspects, like machine learning of complex operational situations, the metrics for quantitative assessment of autonomy, and potential conflicts between autonomy principles and external safety fences can have critical safety impacts and demand further discussions.

Remotely-communicating software-based systems are tightly present in modern industrial society and securing their complex architecture is recognized as crucial. In particular, the perspectives to reinforce their security by monitoring are promising. However, monitoring schemes still face challenges as the presence of untrusted components seems unavoidable. Specially, since untrusted components may be placed in unsupervised areas, making them ideal targets for attackers. In this work, we propose a framework intended to support designers during systems conception. The approach mainly relies upon Security Watchdogs committed to detect and signal distrustful activity. A model-based framework is introduced to ease attacks descriptions upon scenarios in the form of UML sequence diagrams. The scenarios endowed with predefined attack patterns are analyzed using models transformations and symbolic techniques. By doing so, the effectiveness of watchdogs is confronted against attacks and the results can be used to reinforce the overall security of the system. The applicability of the proposed method is also shown by means of a Smart Grid case study.

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.

In early design phases, system models can be characterized as intended interactions between black box components. Moreover, when dealing with embedded systems, it is usual that interactions are constrained by timing issues. We propose to represent such system models as structured scenarios by using UML sequence diagrams specialized with the MARTE profile to handle timing constraints. By using symbolic execution techniques, we show how to analyze these system models and how to extract behavioral constraints concerning components. Those constraints can be used as unitary test purposes to select components of the system.