While the importance of autonomous systems in our daily lives and in the industry increases, we have to ensure that this development is accepted by their users. A crucial factor for a successful cooperation between humans and autonomous systems is a basic understanding that allows users to anticipate the behavior of the systems. Due to their complexity, complete understanding is neither achievable, nor desirable. Instead, we propose self-explainability as a solution. A self-explainable system autonomously explains behavior that differs from anticipated behavior. As a first step towards this vision, we present an approach for detecting anomalous behavior that requires an explanation and for reducing the huge search space of possible reasons for this behavior by classifying it into classes with similar reasons. We envision our approach to be part of an explanation component that can be added to any autonomous system.

The efficient mapping of stream processing applications to parallel hardware architectures is a difficult problem. While parallelization is often highly desirable as it reduces the overall execution time, its advantages must be carefully weighed against the parallelization overhead of complexity and communication costs. This paper presents a novel profile-guided optimization for parallel stream processing based on the multi-paradigm system programming language Rust. Our approach's key idea is to systematically balance the performance gain that can be achieved from parallelization with the communication overhead. To achieve this, we 1) use profiling to gain tight estimates of task execution times, 2) evaluate the cost of the fundamental concurrency constructs in Rust with synthetic benchmarks, and exploit this information to estimate the communication overhead introduced by various degrees of parallelism, and 3) present a novel optimization algorithm that exploits both estimates to fine-tune the degree of parallelism and train processing in a given application. Overall, our approach enables us to map parallel stream processing applications to parallel hardware efficiently. The safety concepts anchored in Rust ensure the reliability of the resulting implementation. We demonstrate our approach's practical applicability with two case studies: the word count problem and aircraft telemetry decoding.

Dynamic Information Flow Control (IFC) systems, like No-Sensitive-Upgrade or Permissive-Upgrade, can guarantee Termination-Insensitive Non-Interference, but reject valid programs due to their inability to track implicit flows. More advanced multi-execution based approaches, like Shadow Execution and Secure Multi-Execution, are precise and guarantee Termination-Sensitive Non-Interference, but require additional resources or, in the case of Faceted Evaluation, deep changes to the execution semantics. In this paper, we propose a novel efficient and precise Information Flow Control system for machine code through Demand-Driven Secure Multi-Execution. Our key idea is to use lightweight single-execution monitoring as long as the execution is secretless and fork multiple copies on-demand when necessary. We present the first Secure Multi-Execution implementation for legacy code in Unix-based environments and show that our demand-driven optimization drastically reduces the run-time overhead for cat and sha256sum. Our results indicate that further acceleration is possible through improved static analyses, making multi-execution based IFC systems applicable to machine code.

Enforcement of hypersafety security policies such as noninterference can be achieved through Secure Multi-Execution (SME). While this is typically very resource-intensive, more efficient solutions such as Demand-Driven Secure Multi-Execution (DDSME) exist. Here, the resource requirements are reduced by restricting multi-execution enforcement to critical sections in the code. However, the current solution requires manual binary analysis. In this paper, we propose a fully automatic critical section analysis. Our analysis extracts a context-sensitive boundary of all nodes that handle information from the reachability relation implied by the control-flow graph. We also provide evaluation results, demonstrating the correctness and acceleration of DDSME with our analysis.

Static worst-case execution time analysis enables to obtain guaranteed timing bounds for programs, which is required for safety-critical hard real-time systems. This comprises micro-architectural analyses that rely on full knowledge of the executed program. An example are current approaches to statically bound the time penalty of mispredicted branches in systems using static or dynamic branch predictors. On the other hand, in artificial software diversity, uncertainty in program aspects is used to render code-reuse attacks useless, making the system considerably more secure. We solve this conflict by proposing adapted static analyses for static and dynamic branch prediction that are able to cope with diversity, and by quantifying the impact of diversity onto the analysis results through extensive evaluation.

The increasing use of closed-source software in everyday life leads to a need for privacy verification of binary code. Unfortunately, analyses of machine code behavior are often imprecise, do not scale, or require expert interaction. We present a novel and fast algorithm that is capable of soundly approximating I/O behavior of binary code. The key idea of our algorithm is that overall I/O behavior can be approximated by analyzing input and output operations. Since most function parameters are defined close to their use, our backward symbolic execution algorithm can quickly recover most meaningful parameters. We show the applicability and performance of our approach by analyzing the coreutils binaries.

Artificial Software Diversity is a well-established method to increase security of computer systems by thwarting code-reuse attacks, which is particularly beneficial in safety-critical real-time systems. However, static worst-case execution time (WCET) analysis on complex hardware involving caches only delivers sound results for single versions of the program, as it relies on absolute addresses for all instructions. To overcome this problem, we present an abstract interpretation based instruction cache analysis that provides a safe yet precise upper bound for the execution of all variants of a program. We achieve this by integrating uncertainties in the absolute and relative positioning of code fragments when updating the abstract cache state during the analysis. We demonstrate the effectiveness of our approach in an in-depth evaluation and provide an overview of the impact of different diversity techniques on the WCET estimations.

A key challenge in cyber-physical systems is to autonomously maintain system goals in the presence of uncertainties concerning the environment behaviour at runtime. Self-adaptivity has shown to be powerful to cope with this. It is usually based on a feedback loop that continuously evaluates the satisfaction of system goals and adapts the system in case of violations. However, most approaches rely on reactive adaptation, where the system triggers adaptations when goals are already violated. In contrast, proactive adaptation anticipates possible goal violations in the future and triggers adaptation in time. To enable this, the system maintains a model that allows for predicting the environment behaviour in the near future. However, these models are often heavyweight and resource-consuming to predict future behaviour (e.g. based on model checking). To overcome this problem, we present a lightweight approach for continuous learning of environment profiles and integrate it with resource-efficient rule-based adaptation. Moreover, we combine proactive adaptation that uses future predictions based on learned profiles, and reactive adaptation. We illustrate our ideas with an autonomous production system.

Simulink and Stateflow are widely-used industrial tools for the development of embedded systems, e.g. in the automotive domain. In modern automotive control systems, multiple components are typically interconnected, and, nowadays, also have a connection to the internet. This poses severe threats, as safety-critical components may be subject to remote attacks, which divert control or information flow from non-critical to safety-critical components. In this paper, we present a novel approach for the analysis of information flow in combined Simulink/Stateflow models. The key idea of our approach is that we analyze the information flow in a given model by computing an over-approximation of the control flow and deduce whether all control flow conditions on a given path combined permit information flow or not. With our approach, we safely rule out the existence of information flow on specific paths. Thus, it enables us to reason about non-interference and the compliance with security policies.

Approaches for the automatic analysis of security policies on source code level cannot trivially be applied to binaries. This is due to the lacking high-level semantics of low-level object code, and the fundamental problem that control-flow recovery from binaries is difficult. We present a novel approach to recover the control-flow of binaries that is both safe and efficient. The key idea of our approach is to use the information contained in security mechanisms to approximate the targets of computed branches. To achieve this, we first define a restricted control transition intermediate language (RCTIL), which restricts the number of possible targets for each branch to a finite number of given targets. Based on this intermediate language, we demonstrate how a safe model of the control flow can be recovered without data-flow analyses. Our evaluation shows that that makes our solution more efficient than existing solutions.

Simulink is widely used in model-driven design.However, the complexity of hybrid systems that are modeled in Simulink limits the applicability of reuse techniques, which impedes cost-efficient design of complex systems. In particular, a systematic use and reuse of complex submodels, e.g. components with varying structure and functionality, is currently not supported. In this paper, we present an approach for service-oriented design in Simulink. The main idea is that we create a modular representation of complex Simulink structures as services with an expressive and formally defined dynamic interface. A dynamic interface captures not only the types of input and output signals but also their discrete and continuous behavior. Our main contribution is threefold: First, we introduce services in Simulink. Second, we transfer the concept of feature modeling to Simulink to express the variability of a service. Third, we introduce the novel concept of hybrid contracts to define the dynamic interface of a service. With our approach, we enable the designer (1) to define hybrid services that are reusable, and (2) to efficiently develop complex hybrid systems from a given set of services. We demonstrate this with a case study of a hybrid temperature control system.

A key challenge in cyber-physical systems is their highly dynamic nature including changing system goals. Therefore, these systems have to autonomously manage their system goals and continuously evaluate their achievement at run-time. However, with the increasing complexity of system goals including, e.g., priorities, dependencies, and conflicts among goals, a binary or qualitative judgement of achievement of goals is not sufficient anymore. Instead, it is necessary to quantify the degree to which the goals are fulfilled in order to balance the cost-benefit ratio at run-time. In this paper, we present a hierarchical and modular goal model that allows for capturing complex relations between subgoals, e.g., dependencies and conflicts. We provide an algorithm that efficiently evaluates gradual achievement of goals at run-time. Due to the modular structure of our model and our evaluation, goals can easily be added, removed, and changed at run-time. With our approach, we a) ease the design of goal-aware autonomous systems by providing an explicit structure that emphasises relations between subgoals, b) provide an automatic quantification of the satisfaction of complex system goals that can be used to, e.g., evaluate autonomous decisions at runtime, and c) enable runtime management of changing system goals.

Current methods for planning in real-time environments only consider planning goals with a restricted expressiveness, even those using the temporal logic Timed CTL (TCTL). These approaches support TCTL subsets expressing rather simple reachability goals and safety properties, but do not allow the arbitrary nesting and conjunction of TCTL formulas. However, this is a serious drawback in many practical applications. An example are medical systems that have to repeat an action infinitely often within given time bounds. To close this gap, we provide an algorithm for planning with these goals by adapting concepts from symbolic model checking. Hence, we can automatically generate plans fulfilling more complex tasks within a real-time context, while improving safety and efficiency by using formally founded model checking methods.

SystemC is widely used for modeling and simulation in hardware/software co-design. However, existing verification techniques are mostly ad-hoc and non-systematic. In this article, we present a systematic, comprehensive, and formally founded co-verification framework for digital HW/SW systems that are modeled in SystemC. The framework is based on a formal semantics of SystemC and uses a combination of model checking and testing, whereby testing includes both the automated generation of timed inputs and automated conformance evaluation. We demonstrate its performance and its error detecting capability with two case studies, namely a packet switch and an anti-slip regulation and anti-lock braking system.

MATLAB Simulink is the most widely used industrial tool for developing complex embedded systems in the automotive sector. The resulting Simulink models often consist of more than ten thousand blocks and a large number of hierarchy levels. To ensure the quality of such models, automated static analyses and slicing are necessary to cope with this complexity. In particular, static analyses are required that operate directly on the models. In this article, we present an approach for slicing Simulink Models using dependence graphs and demonstrate its efficiency using case studies from the automotive and avionics domain. With slicing, the complexity of a model can be reduced for a given point of interest by removing unrelated model elements, thus paving the way for subsequent static quality assurance methods.

Systematically enumerating derivations of a grammar yields for realistic grammars test sets that are to large to be tested with reasonable costs. Existing reduction techniques for grammar-based testing guide the enumeration process to restrict the number of generated test cases. However, they do not provide a rule coverage criterion, i.e., they do not aim at providing a test set that ensures coverage of t-wise rule combinations. Selecting derivations such that all possible t-wise rule combinations are covered with at least one test case allows for the generation of small test sets. We employ combinatorial interaction testing to generate the test sets and derive the necessary test specification from the grammar specification automatically. Our evaluation results are twofold. First, they demonstrate the efficiency of our approach. Second, they reveal shortcomings of existing tools for combinatorial interaction testing with constraints.

Process algebras like Timed CSP offer a convenient level of abstraction for the specification and verification of distributed embedded real-time systems. Complex systems can be specified in terms of interacting modules whose interaction can be analyzed using the mechanisms of the process algebra. In this paper, we present a development approach that supports the construction of distributed real-time systems by exploiting Timed CSP's concept of modularity. Individual system components are refined to their low-level implementations and shown to be a formally correct implementation of their respective Timed CSP specifications. Their interaction can then be analyzed by composing the individual process specifications. The key idea underlying the presented approach is a formal relation between timed process algebraic specifications and implementations given in a general purpose programming language.

In safety-critical applications, the real-time behavior is crucial for the correctness of the overall system and must be tested thoroughly. However, the generation of test traces that cover most or all of the desired behavior of a real-time system is a difficult challenge. In this paper, we present an evolutionary algorithm that generates timed test traces, which achieve a given transition coverage. We generate these traces from a timed automata model. Our main contribution is a novel approach to encode timed test traces as individuals of an evolutionary algorithm. The major difficulty in doing so is that test traces for embedded real-time systems have to be very long. To solve this problem, we introduce the notion of blocks, which simplify long traces by cutting them into pieces. With that, we reduce the search space significantly. Furthermore, we have implemented crossover and mutation operators and a fitness function that takes time-dependent behavior implicitly into account. We show the success of our approach by experimental results from an anti-lock braking system.

The SystemC Transaction Level Modeling (TLM) standard is widely used for modeling and simulation in hardware/software co-design. However, the semantics of the TLM core interfaces is only informally defined. This makes it impossible to apply formal verification techniques to transaction level models that conform to the TLM standard. To solve this problem, we propose a formal semantics of the TLM transport mechanisms using timed automata. We achieve this by providing a set of timed automata templates that precisely capture the semantics of the TLM core interfaces. Then, we use this set to transform a given SystemC-TLM model into a semantically equivalent timed automata model. The transformation is an extension of our previously proposed transformation from SystemC into Uppaal timed automata and can be used to verify safety, liveness, and timing properties of TLM models using the Uppaal model checker. We demonstrate the applicability and performance of our approach with two case studies, namely a loosely-timed model that uses a blocking transport and an approximately-timed model that uses a 4-phase non-blocking transport.

Process Networks (PNs) are used for modeling streaming-oriented applications with changing behavior, which must be mapped on a concurrent architecture to meet the performance and energy constraints of embedded devices. Finding an optimal mapping of Process Networks to the constrained architecture presumes that the behavior of the PN is statically known. In this paper we present a static analysis for synchronous PNs that partitions the state space according to extract run-time modes based on a Data Augmented Control Flow Automaton (DACFA). The result is a mode automaton whose nodes describe identified program modes and whose edges represent transitions among them. Optimizing back-ends mapping from PNs to concurrent architectures can be guided by these analysis results.

SystemC is widely used for modeling and simulation in hardware/software co-design. However, the co-verification techniques used for SystemC designs are mostly ad-hoc and non-systematic. A particularly severe drawback is that simulation results have to be evaluated manually. In previous work, we proposed to overcome this problem by conformance testing. We presented an algorithm that uses an abstract SystemC design to compute expected output traces, which are then compared with those of a refined design to evaluate its correctness. The main disadvantage of the algorithm is that it is very expensive because it computes the output traces offline and has to cope with non-deterministic systems. Furthermore, the designer has to compare the results manually with the outputs of a design under test. In this paper, we present an approach for efficient and fully-automatic conformance evaluation of SystemC designs. To achieve this, we first present optimizations of our previously proposed algorithm for the generation of conformance tests that drastically reduce computation time and memory consumption. The main idea is to exploit the specifics of the SystemC semantics to reduce the number of semantic states that have to be kept in memory during state-space exploration. Second, we present an approach to generate SystemC test benches from a set of expected output traces. These test benches allow fully-automatic test execution and conformance evaluation. Together with our previously presented model checking framework for abstract Sys-temC designs, we yield a fully-automatic HW/SW co-verification framework for SystemC that supports the whole design process. We demonstrate the performance and error detecting capability of our approach with experimental results.

Many software faults are triggered by unusual combinations of input values and can be detected using pairwise test sets that cover each pair of input values. The generation of pairwise test sets with a minimal size is an NP-complete problem which implies that many algorithms are either expensive or based on a random process. In this paper we present a deterministic algorithm that exploits our observation that the pairwise testing problem can be modeled as a k-partite graph problem. We calculate the test set using well investigated graph algorithms that take advantage of properties of k-partite graphs. We present evaluation results that prove the applicability of our algorithm and discuss possible improvement of our approach.

Real-time systems often have to cope with an unbounded number of components. For example, an operating system scheduler has to be able to manage an arbitrary number of threads. At the same time, the correctness of central control units such as schedulers is crucial for the correctness of the whole system. However, the comprehensive and semi-automatic verification of real-time systems that are parameterized with an unbounded number of components is still an open problem. In this paper, we propose an approach in which parameterized systems can be verified using a combination of theorem proving and model checking. The interactive theorem prover is used for the overall verification task delegating subsequent proof-goals to automatic verification tools. The central proof method is based on network invariants. The idea of network invariants is to over approximate all instances of a parameterized system and to perform the verification on the abstract model. We have adopted an existing network invariant approach for the verification of centralized real-time systems such as schedulers and formalized the theory in the Isabelle/HOL theorem prover. Preliminary results on applying our framework to small examples are promising and make it worth to evaluate the approach with larger case studies in future work.

In this paper, we applied our approach for verifying low-level code to the scheduler of the real-time operating system BOSS. We developed its high-level specification in CSP-OZ and showed that it enforces the BOSS scheduling strategy. Furthermore, we presented a low-level CSPMmodel, which has been semi-automatically synthesized from its implementation. Using the automatic FDR2 refinement checker, we proved that the low-level model is a failures-divergence refinement of the CSPMencoding of the scheduler's CSP-OZ specification. First, this means that the methods are terminating. Second, the implementation respects the pre- and post-conditions of its specification. Third, the implementation produces exactly the schedules that are described by the CSP-OZ specification. We intend to examine other components of BOSS using our approach. Another objective is to extend it to enable the verification of real-time systems by using our formalization of Timed CSP in the Isabelle/HOL theorem prover [T. Gothel and S. Glesner, 2009].

Abstract Even though computations on finite integer representations are as old as computers themselves, there is one problem that has been inexcusably neglected: integer computations in programming languages do not operate on the ring [inline-graphic not available: see fulltext] of integer numbers but only on finite subsets of it. Changing the size of integer representations may change the results of operations performed on them in unexpected ways. In particular, increasing the representation size of intermediate results during computation may lead to incorrect final results. In this paper, we develop an algebraic foundation for integer arithmetic under changing representation sizes and, in particular, a criterion for safely replacing one finite integer arithmetic by another. This safety criterion has also been verified in the theorem prover Isabelle/HOL. Based on this formal development, we not only reveal and explain an inconsistency in the Java Card integer arithmetic but also propose an optimization for Java Card integer expressions and their safe transformation into Java Card bytecode. We also discuss the application of this safety criterion to constant folding, a standard compiler optimization, for Java and C compilers.

Correct compilers are a vital precondition to ensure software correctness. Optimizations are the most error-prone phases in compilers. In this paper, we formally verify dead code elimination (DCE) within the theorem prover Isabelle/HOL. DCE is a popular optimization in compilers which is typically performed on the intermediate representation. In our work, we reformulate the algorithm for DCE so that it is applicable to static single assignment (SSA) form which is a state of the art intermediate representation in modern compilers, thereby showing that DCE is significantly simpler on SSA form than on classical intermediate representations. Moreover, we formally prove our algorithm correct within the theorem prover Isabelle/HOL. Our program equivalence criterion used in this proof is based on bisimulation and, hence, captures also the case of non-termination adequately. Finally we report on our implementation of this verified DCE algorithm in the industrial-strength scale compiler system.

Natural semantics specifications have become mainstream in the formal specification of programming language semantics during the last 10 years. In this article, we set up sorted natural semantics as a specification framework which is able to express static semantic information of programming languages declaratively in a uniform way and allows one at the same time to generate corresponding analyses. Such static semantic information comprises context-sensitive properties which are checked in the semantic analysis phase of compilers as well as further static program analyses such as, for example, classical data and control flow analyses or type and effect systems. The latter require fixed-point analyses to determine their solutions. We show that, given a sorted natural semantics specification, we can generate the corresponding analysis. Therefore, we classify the solution of such an analysis by the notion of a proof tree. We show that a proof tree can be computed by solving an equivalent residuation problem. In case of the semantic analysis, this solution can be found by a basic algorithm. We show that its efficiency can be enhanced using solution strategies. We also demonstrate our prototype implementation of the basic algorithm which proves its applicability in practical situations. With the results of this article, we have established natural semantics as a framework which closes the gap between declarative and operational specification methods for static semantic properties as well as between specification frameworks for the semantic analysis. In particular, we show that natural semantics is expressive enough to define fixed-point program analyses.