This work introduces Information Inference Diagrams (I2Ds), a modeling framework aiming to complement existing approaches for privacy and security analysis of distributed systems. It is intended to support established threat modeling processes. Our approach is designed to be compatible with Data Flow Diagrams (DFDs), which form the basis of many established techniques and tools. Unlike DFDs, I2Ds represent information propagation, going beyond mere data flows to enable more formal reasoning in threat modeling while remaining practical. They define inference and sharing (flow) relations on information items to model how information moves through a system. To this end, we provide formal definitions for information items, entities, and flows. By introducing classes as a type system, our formal rules are both generic and allow conformance to existing vocabularies. We demonstrate the applicability of I2Ds through examples, that showcase their versatility in system analysis.

The design of reinforcement learning (RL) agents is difficult, especially in domains with complex and possibly conflicting objectives such as autonomous driving. In addition to the formal nature of RL with high technical barriers, the fragility of the reward signal results in the common trial-and-error practice in the design of RL agents. We propose a novel goal-oriented specification language that is tailored to reinforcement learning but abstracts from technical details. To overcome the problematic trial-and-error practice, our specification language provides the foundation for an easy and systematic design process in RL.

Active automata learning (AAL) algorithms infer accurate automata models of black box applications, letting developers verify the behavior of increasingly complex real-time systems (RTS). However, learning models of larger RTS often takes very long or is not feasible at all. We introduce Mealy machines with local timers , a new class of Mealy machines that permit multiple location-bound timers and that can be learned efficiently. We design an efficient learning algorithm for them and validate our method across diverse case studies ranging from automotive systems to smart home appliances, where we drastically reduce runtimes compared to the state-of-the-art approach, thus, making AAL available for a wide range of RTS.

Active automata learning algorithms like TTT infer accurate automata models of black-box applications and thereby help developers to understand the behavior of increasingly complex cyber-physical systems. However, learning systems with large input alphabets often takes very long or is not feasible at all. We present TTT/ik, an extension of TTT that exploits an imprecise symbol filter that uses imprecise prior knowledge of state local alphabets to learn accurate Mealy automata more efficiently. We show across seven realistic case studies that our method almost always dramatically reduces queries and symbols even with imprecise knowledge, while still being accurate, thus, greatly improving runtime in practice.

The need for systems to explain behavior to users has become more evident with the rise of complex technology like machine learning or self-adaptation. In general, the need for an explanation arises when the behavior of a system does not match the user’s expectations. However, there may be several reasons for a mismatch including errors, goal conflicts, or multi-agent interference. Given the various situations, we need precise and agreed descriptions of explanation needs as well as benchmarks to align research on explainable systems. In this paper, we present a taxonomy that structures needs for an explanation according to different reasons. We focus on explanations to improve the user interaction with the system. For each leaf node in the taxonomy, we provide a scenario that describes a concrete situation in which a software system should provide an explanation. These scenarios, called explanation cases, illustrate the different demands for explanations. Our taxonomy can guide the requirements elicitation for explanation capabilities of interactive intelligent systems and our explanation cases build the basis for a common benchmark. We are convinced that both, the taxonomy and the explanation cases, help the community to align future research on explainable systems.

The key advantage of autonomous car platoons are their short inter-vehicle distances that increase traffic flow and reduce fuel consumption. However, this is challenging for operational and functional safety. If a failure occurs, the affected vehicles cannot suddenly stop driving but instead should continue their operation with reduced performance until a safe state can be reached or, in the case of temporal failures, full functionality can be guaranteed again. To achieve this degradation, platoon members have to be able to compensate sensor and communication failures and have to adjust their inter-vehicle distances to ensure safety. In this work, we describe a systematic design of degradation cascades for sensor and communication failures in autonomous car platoons using the example of an autonomous model car. We describe our systematic design method, the resulting degradation modes, and formulate contracts for each degradation level. We model and test our resulting degradation controller in Simulink/Stateflow.

Embedded systems usually consist of deeply integrated hardware and software components. As a consequence, modular verification is not easily possible. One important step towards modular verification of integrated HW/SW systems is to automatically compute abstractions of components that influence the overall system behavior but are not relevant for a given property. In this paper, we present an automatic abstraction technique for HW/SW co-designs modeled in SystemC. The key idea is to use a variant of classical abstract interpretation that is tailored for the specific semantics of SystemC. Our main contributions are the following: First, we present an analysis that determines data-dependencies between variables and equivalent data values with respect to conditional branches while taking the timing behavior and scheduling policies of SystemC into consideration. Second, we use the results for slicing and variable abstraction to significantly reduce the semantic state space of a given SystemC design and again produce a valid abstract design. Our abstraction technique makes it possible to automatically verify properties for comparatively large designs with the UPPAAL model checker, which cannot be handled without our approach. We demonstrate this with two case studies from the SystemC reference implementation.

Embedded software is concurrent, real-time dependent, typically networked, must meet strict resource and high quality requirements, and often runs on cheap hardware. Altogether, this makes the education of embedded software designers a difficult challenge. In this paper, we present an embedded software design project, where students have to develop a multi-robot search using Lego mindstorms. The main idea is to confront the students with all the spites that are typically present in embedded systems, while at the same time giving them an algorithmically non-trivial problem to solve. To this end, we let the students use a bio-inspired search algorithm (particle-swarm optimization) to detect survivors (led by cries for help) in an unknown disaster zone using a number of Lego Mindstorm robots. We have executed this project simultaneously at the University of Potsdam and TU Berlin and discuss results and evaluations. We think that this project is very well suited for the education of embedded software engineers.

Memory safety plays a crucial role in concurrent hardware/software systems and must be guaranteed under all circumstances. Although there exist some approaches for complete verification that can cope with both hardware and software and their interplay, none of them supports pointers or memory. To overcome this problem, we present a novel approach for model checking memory-related properties of digital HW/SW systems designed in SystemC/TLM. The main idea is to formalize a clean subset of the SystemC memory model using Uppaal timed automata. Then, we embed this formal memory model into our previously proposed automatic transformation from SystemC/TLM to Uppaal timed automata. With that, we can fully automatically verify memory-related properties of a wide range of practical applications. We show the applicability of our approach by verifying memory safety of an industrial design that makes ample use of pointers and call-by-reference.