Industrial analytics – An overview

The digital transformation generates huge amounts of heterogeneous data across the industrial value chain, from simulation data in engineering, over sensor data in manufacturing to telemetry data on product use. Extracting insights from these data constitutes a critical success factor for industrial enterprises, e. g., to optimize processes and enhance product features. This is referred to as industrial analytics, i. e., data analytics for industrial value creation. Industrial analytics is an interdisciplinary subject area between data science and industrial engineering and is at the core of Industry 4.0. Yet, existing literature on industrial analytics is fragmented and specialized. To address this issue, this paper presents a holistic overview of the field of industrial analytics integrating both current research as well as industry experiences on real-world industrial analytics projects. We define key terms, describe typical use cases and discuss characteristics of industrial analytics. Moreover, we present a conceptual framework for industrial analytics that structures essential elements, e. g., data platforms and data roles. Finally, we conclude and highlight future research directions.

Towards Human-Centered AI: Psychological concepts as foundation for empirical XAI research

Human-Centered AI is a widely requested goal for AI applications. To reach this is explainable AI promises to help humans to understand the inner workings and decisions of AI systems. While different XAI techniques have been developed to shed light on AI systems, it is still unclear how end-users with no experience in machine learning perceive these. Psychological concepts like trust, mental models, and self-efficacy can serve as instruments to evaluate XAI approaches in empirical studies with end-users. First results in applications for education, healthcare, and industry suggest that one XAI does not fit all. Instead, the design of XAI has to consider user needs, personal background, and the specific task of the AI system.

Bayesian hybrid automata: Reconciling formal methods with metrology

Hybrid system dynamics arises when discrete actions meet continuous behaviour due to physical processes and continuous control. A natural domain of such systems are emerging smart technologies which add elements of intelligence, co-operation, and adaptivity to physical entities. Various flavours of hybrid automata have been suggested as a means to formally analyse dynamics of such systems. In this article, we present our current work on a revised formal model that is able to represent state tracking and estimation in hybrid systems and thereby enhancing precision of verification verdicts.

Functional verification of cyber-physical systems containing machine-learnt components

Functional architectures of cyber-physical systems increasingly comprise components that are generated by training and machine learning rather than by more traditional engineering approaches, as necessary in safety-critical application domains, poses various unsolved challenges. Commonly used computational structures underlying machine learning, like deep neural networks, still lack scalable automatic verification support. Due to size, non-linearity, and non-convexity, neural network verification is a challenge to state-of-art Mixed Integer linear programming (MILP) solvers and satisfiability modulo theories (SMT) solvers [2], [3]. In this research, we focus on artificial neural network with activation functions beyond the Rectified Linear Unit (ReLU). We are thus leaving the area of piecewise linear function supported by the majority of SMT solvers and specialized solvers for Artificial Neural Networks (ANNs), the successful like Reluplex solver [1]. A major part of this research is using the SMT solver iSAT [4] which aims at solving complex Boolean combinations of linear and non-linear constraint formulas (including transcendental functions), and therefore is suitable to verify the safety properties of a specific kind of neural network known as Multi-Layer Perceptron (MLP) which contain non-linear activation functions.

System correctness under adverse conditions

This special issue presents seven overview articles on research conducted in the Research Training Group “System Correctness under Adverse Conditions” (SCARE) at the University of Oldenburg.

A sampling-based approach for handling delays in continuous and hybrid systems

Delays in feedback dynamics of coupled dynamical systems arise regularly, especially in embedded control where the physical plant and the controller continuously interact through digital networks. Systems featuring delays are however notoriously difficult to analyze. Consequently, formal analysis often addresses simplified, delay-free substitute models, risking negligence of the adverse impact of delay on control performance. In this ongoing work, we demonstrate that for continuous systems such as delay differential equations, a major part of the delay-induced complexity can be reduced effectively when adding natural constraints to the model of the delayed feedback channel, namely that it transports a band-limited signal and implements a non-punctual, distributed delay. The reduction is based on a sampling approach which is applicable when the above conditions on the feedback are satisfied. We further discuss the possibilities of lifting this method to mixed discrete-continuous dynamics of delayed hybrid systems and the open issues thereof.

Infinite-state graph transformation systems under adverse conditions

We present an approach for modeling adverse conditions by graph transformation systems. To this end, we introduce joint graph transformation systems which involve a system, an interfering environment, and an automaton modeling their interaction. For joint graph transformation systems, we present notions of correctness under adverse conditions. Some instances of correctness are expressible in LTL (linear temporal logic), or in CTL (computation tree logic), respectively. In these cases, verification of joint graph transformation systems is reduced to temporal model checking. To handle infinite state spaces, we incorporate the concept of well-structuredness. We discuss ideas for the verification of joint graph transformation systems using results based on well-structuredness.

Proving properties of autonomous car manoeuvres in urban traffic

As automated driving techniques are increasingly capturing the market, it is particularly important to consider vital functional properties of these systems. We present an overview of an approach that uses an abstract model to logically reason about properties of autonomous manoeuvres at intersections in urban traffic. The approach introduces automotive-controlling timed automata crossing controllers that use the traffic logic UMLSL (Urban Multi-lane Spatial Logic) to reason about traffic situations. Safety in the context of collision freedom is mathematically proven. Liveness (something good finally happens) and fairness (no queue-jumping) are examined and verified using a model-checking tool for timed automata, UPPAAL.

Exploiting symmetries of high-level Petri games in distributed synthesis

Distributed Synthesis is the problem of automatically generating correct controllers for individual agents in a distributed system. Petri games model this problem by a game between two teams of players on a Petri net structure. Under some restrictions, Petri games can be solved by a reduction to a two player game. The concept of symmetries in Petri nets is closely related to high-level representations of Petri games. Applying symmetries to the states in the two-player game results in a significant state space reduction. We give an overview about (high-level) Petri games and the application of symmetries in this setting. We present ongoing work aiming to concisely describe solutions of Petri games by a high-level representation.

Abstraction NBTI model

Negative Bias Temperature Instability (NBTI) is one of the major transistor aging effects, possibly leading to timing failures during run-time of a system. Thus one is interested in predicting this effect during design time. In this work an Abstraction NBTI model is introduced reducing the state space of trap-based NBTI models using two abstraction parameters, applying a state transformation to incorporate variable stress conditions. This transformation is faster than traditional approaches. Currently the conversion into estimated threshold voltage damages is a very time consuming process.