Abstract Many systems can be expressed as multivariate state sequences (MSS) in terms of entities and their states with evolving dependencies over time. In order to interpret the temporal dynamics in such data, it is essential to capture relationships between entities and their changes in state and dependence over time under uncertainty. Existing probabilistic models do not explicitly model the evolution of causality between dependent state sequences and mostly result in complex structures when representing complete causal dependencies between random variables. To solve this, Temporal State Change Bayesian Networks (TSCBN) are introduced to effectively model interval relations of MSSs under evolving uncertainty. Our model outperforms competing approaches in terms of parameter complexity and expressiveness. Further, an efficient structure discovery method for TSCBNs is presented, that improves classical approaches by exploiting temporal knowledge and multiple parameter estimation approaches for TSCBNs are introduced. Those are expectation maximization, variational inference and a sampling based maximum likelihood estimation that allow to learn parameters from partially observed MSSs. Lastly, we demonstrate how TSCBNs allow to interpret and infer patterns of captured sequences for specification mining in automotive.

Verification is essential to prevent malfunctioning of software systems. Model checking allows to verify conformity with nominal behavior. As manual definition of specifications from such systems gets infeasible, automated techniques to mine specifications from data become increasingly important. Existing approaches produce specifications of limited lengths, do not segregate functions and do not easily allow to include expert input. We present BaySpec, a dynamic mining approach to extract temporal specifications from Bayesian models, which represent behavioral patterns. This allows to learn specifications of arbitrary length from imperfect traces. Within this framework we introduce a novel extraction algorithm that for the first time mines LTL specifications from such models.

Contextual anomalies arise only under special internal or external stimuli in a system, often making it infeasible to detect them by a rule-based approach. Labelling the underlying problem sources is hard because complex, time-dependent relationships between the inputs arise. We propose a novel unsupervised approach that combines tools from deep learning and signal processing, working in a purely data-driven way. Many systems show a desirable target behaviour which can be used as a proxy quantity removing the need to manually label data. The methodology was evaluated on real-life test car traces in the form of multivariate state message sequences. We successfully identified contextual anomalies during the cars' timeout process along with possible explanations. Novel input encodings allow us to summarise the entire system context including the timing such that more information is available during the decision process.

In modern vehicles, high communication complexity requires cost-effective integration tests such as data-driven system verification with in-vehicle network traces. With the growing amount of traces, distributable Big Data solutions for analyses become essential to inspect massive amounts of traces. Such traces need to be processed systematically using automated procedures, as manual steps become infeasible due to loading and processing times in existing tools. Further, trace analyses require multiple domains to verify the system in terms of different aspects (e.g., specific functions) and thus, require solutions that can be parameterized towards respective domains. Existing solutions are not able to process such trace amounts in a flexible and automated manner. To overcome this, we introduce a fully automated and parallelizable end-to-end preprocessing framework that allows to analyze massive in-vehicle network traces. Being parameterized per domain, trace data is systematically reduced and extended with domain knowledge, yielding a representation targeted towards domain-specific system analyses. We show that our approach outperforms existing solutions in terms of execution time and extensibility by evaluating our approach on three real-world data sets from the automotive industry.

With the increasing amount of interconnections between vehicles, the attack surface of internal vehicle networks is rising steeply. Although these networks are shielded against external attacks, they often do not have any internal security to protect against malicious components or adversaries who can breach the network perimeter. To secure the in-vehicle network, all communicating components must be authenticated, and only authorized components should be allowed to send and receive messages. This is achieved through the use of an authentication framework. Cryptography is widely used to authenticate communicating parties and provide secure communication channels (e.g., Internet communication). However, the real-time performance requirements of in-vehicle networks restrict the types of cryptographic algorithms and protocols that may be used. In particular, asymmetric cryptography is computationally infeasible during vehicle operation. In this work, we address the challenges of designing authentication protocols for automotive systems. We present Lightweight Authentication for Secure Automotive Networks (LASAN), a full lifecycle authentication approach. We describe the core LASAN protocols and show how they protect the internal vehicle network while complying with the real-time constraints and low computational resources of this domain. By leveraging the fixed structure of automotive networks, we minimize bandwidth and computation requirements. Unlike previous work, we also explain how this framework can be integrated into all aspects of the automotive product lifecycle, including manufacturing, vehicle maintenance, and software updates. We evaluate LASAN in two different ways: First, we analyze the security properties of the protocols using established protocol verification techniques based on formal methods. Second, we evaluate the timing requirements of LASAN and compare these to other frameworks using a new highly modular discrete event simulator for in-vehicle networks, which we have developed for this evaluation.