Test-suite reduction targets to find a minimal subset of the test suite that is sufficient regarding specific test requirements. In general, test-suite reduction causes some kind of loss in the fault-detection ability of the reduced test suite. Cost-Effectiveness for test-suite reduction is only given if the trade-off between the savings in the testing effort and the resulting degradation in the fault-detection ability is reasonable. In this work we define a cost function, summarizing the beneficial output of a test suite depending on the test effort and the fault-detection ability. We apply this cost function to test suites that are defined by different commonly used coverage criteria, like MCC (multiple condition coverage), MC/DC (modified condition/decision coverage), and DC (decision coverage) and evaluate the cost function for a safety-relevant system from automotive. The results mainly demonstrate two fundamental aspects of test-suite reduction: First, the cost effectiveness is very sensitive to the assumed costs for the test-case execution and the penalty for undetected faults. Secondly, for non-safety-relevant systems test-suite reduction for DC is still cost effective, but this does not hold for safety-relevant systems. The cost effectiveness of test-suite reduction for safety-relevant systems for MCC and MC/DC is almost the same.

Internet of Things represents a challenge in the automotive industry development, as it demands for innovation, integration, safety and security. These lead to highly sophisticated requirements set for the design process. The difficulty of managing natural language requirements may lead to inherent errors such as incompleteness, ambiguousness, etc. Adding formality to the requirements is recognized by the community to overcome these drawbacks. In this paper, we present a methodology for SoC design support by introducing semi-formalization to the requirements. The methodology allows the reuse by defining requirements patterns for the most frequently used components or mechanisms. The reuse of the requirement patterns drastically decreases the semi-formalization time and covers 60% of reusable components requirements. The methodology is applied on sophisticated automotive application: Airbag System.

Formal methods are a means for verification and validation with the main advantage that a system property can be verified for the overall system (including all possible system states). The drawbacks of formal methods are the additional effort for the formalisation of the requirements and for building a model of the system, and, the limitations due to computational restrictions (handling the state-space explosion). ISO 26262 Road Vehicles - Functional Safety is a standard for the assessment of the development process for safety-relevant components in the automotive domain. The standard addresses formal methods for the specification of safety requirements and for the product development at software level. Formal methods for the hardware development or at system level are (by now) not explicitly foreseen by the standard. In this work we will give an overview on the basic principles and the state-of-the-art of formal methods (in detail, model checking). Then we will present different approaches for the application of formal methods at system level including some preliminary evaluation results for an industrial use case. Based on these experiences we will discuss the applicabi lity of formal methods in the context of ISO 26262 (i.e., for automotive components) in view of the limitations of formal techniques for applications inthe automotive domain

As systems and electrical and electronic devices are becoming more and more complex, the number of requirements is increased accordingly. Therefore, the organization, the processing and the verification of requirements has become a necessity. In automotive applications, this necessity is more pronounced because of the safety regulations imposed by authorities. Semi-formal representation is an approach that helps making the requirements more understandable and rigorous. In particular, SysML has proved to have the capabilities to represent requirements, structure and behaviour of systems and devices in a diagram-based fashion, enabling the linking different elements that define the composition and the functionalities of the desired product. While for software systems and digital hardware it has been applied successfully, very little work has yet been done for analogue and analogue-mixed signal devices. This is mainly because of the particular behaviour of such devices and the continuous quantities related to them. In this paper, we describe the modelling of requirements for an electronic power switch in SysML. We show that the description of the requirements for analogue devices is possible and emphasize its utility in a real scenario.

Modified condition/decision coverage (MC/DC) is a structural code coverage metric, originally defined in the standard DO-178B, intended to be an efficient coverage metric for the evaluation of the testing process of software incorporating decisions with complex Boolean expressions. The upcoming standard ISO 26262 for safety-relevant automotive systems prescribes MC/DC for ASIL D as a highly recommended coverage metric. One assumed benefit of MC/DC is that it requires a much smaller number of test cases in comparison to multiple condition coverage (MCC), while sustaining a quite high error-detection probability. Programming languages like C, commonly used for implementing software for the automotive domain, are using short-circuit evaluation. For short-circuit evaluation the number of test cases for MCC is much smaller than in a non-short-circuit environment because many redundant test cases occur. We evaluated the trade-off between the number of test cases for MCC and MC/DC for a case study from the automotive domain and observed a very low overhead (only 5 %) for the number of test cases necessary for MCC compared to MC/DC. This motivated an analysis of programs containing decisions where the number and structure of the referring Boolean expressions vary. Our results show that the overhead for a test suite for MCC is on the average only about 35 % compared to MC/DC and the maximum overhead is approximately 100 % (for decisions with up to 5 conditions). This means that a test set for MCC is in the worst case around twice as big as a test set for MC/DC for a program with short-circuit evaluation with maximum 5 conditions. Considering the lower error-detection effectiveness of MC/DC compared to MCC, we conclude with the strong recommendation to use MCC as a coverage metric for testing safety-relevant software (with a limited number of conditions) implemented in programming languages with short-circuit evaluation.

System integration testing is the process of testing a system by the stepwise integration of sub-components. Usually these sub-components are already verified to guarantee their correct functional behavior. By integration of these verified subcomponents into the overall system, emergent behavior may occur, i.e. behavior that evolves by the assembling of the subcomponents. For system integration testing, both, the correct functional behavior of the overall system, and, the proper functioning of the sub-components in their system environment, have to be verified. In this work we present the idea of an approach for system integration testing based on formal verification. The system components are modeled in SystemC. In a first step these components are formally verified. Then a model of the overall system is built. In a second step this system model is formally verified. The novelty of this approach is given by two aspects: First, up to now the available verification frameworks for SystemC-models are more a proof of concept than really applicable to real industrial case studies. Secondly, although formal verification techniques are a common technique for the verification of software and hardware, by now they have only marginally considered for system integration testing.

SystemC is a de-facto industry standard for developing, modelling, and simulating embedded systems. As embedded systems become more and more integrated into many aspects of human lives (e.g., transportation, surveillance systems, ...), failures of embedded systems might cause dangerous hazards to individuals or groups. Guaranteeing safety of such systems makes formal verification crucial. In this paper we present a novel approach for verifying SystemC models with SPIN. Focusing on system-level verification we reuse compiled and executable code from the original model and embed it into the verifier generated by SPIN. In contrast to most other approaches, which require a complete model transformation, in our approach the transformation focuses only on the relevant parts of the model while leaving functional blocks untransformed. Our technique aims at reducing the state vector size managed by the verifier of SPIN, at improving state exploration performance by avoiding unnecessary model transformation steps, and at concentrating on verifying properties that emerge from the composition of multiple functional units.

Chilenski and Miller [1] claim that the error detection probability of a test set with full modified condition/decision coverage (MC/DC) on the system under test converges to 100

The testing process for safety-critical systems is usually evaluated with code coverage criteria such as MC/DC (Modified Condition/Decision Coverage) defined in the standard DO-178B, Software Considerations in Airborne Systems and Equipment Certification (a de-facto standard for certifying software in the civil avionic domain). For requirements-based testing techniques we work on coverage metrics that are defined on a higher level of program representation (eg on the requirements), and that are independent of a specific implementation. For that purpose we analyse the relationship between existing definitions for structural requirement-coverage metrics and structural code-coverage metrics. In addition, we work on techniques that preserve structural codecoverage between different program-representation levels.

ion Techniques for Extracted Automata Models Susanne Kandl Institute of Computer Engineering Vienna University of Technology Vienna, Austria Email: susanne@vmars.tuwien.ac.at Abstract — In this paper we present the application of abstraction techniques for automata models. We give an overview on a state-of-the-art method to reduce the complexity of an automaton model without loosing essential information on the behavior of the modeled system (predicate abstraction). We focus on the applicability of the presented methods, especially on models that are directly extracted from the C source code of a system. We present the process for automated model extraction that yields an automaton model we can use for a verification and testing framework. We show how to apply different abstraction techniques on a case study from the automotive domain and evaluate the resulting state space reduction. In this paper we present the application of abstraction techniques for automata models. We give an overview on a state-of-the-art method to reduce the complexity of an automaton model without loosing essential information on the behavior of the modeled system (predicate abstraction). We focus on the applicability of the presented methods, especially on models that are directly extracted from the C source code of a system. We present the process for automated model extraction that yields an automaton model we can use for a verification and testing framework. We show how to apply different abstraction techniques on a case study from the automotive domain and evaluate the resulting state space reduction.

In this paper, we introduce an approach for automated verification and testing of ANSI C programs for embedded systems. We automatically extract an automaton model from the C code of the SUT (system under test). This automaton model is on the one hand used for formal verification of the requirements defined in the system specification, on the other hand, we can derive test cases from this model, for both methods we use a model checker. We describe our techniques for test case generation, based on producing counterexamples with a model checker by formulating trap properties. The resulting test cases can then be applied to the SUT on different test levels. An important issue for model checking C-source code, is the correct modeling of the semantics of a C program for an embedded system. We focus on challenges and possible restrictions that appear, when model checking is used for the verification of C-source code. We specifically show how to deal with arithmetic expressions in the model checker NuSMV and how to preserve the numerical results in case of modeling the platform-specific semantics of C

In this paper we introduce the development of a framework for testing safety-critical embedded systems based on the concepts of model-based testing. In model-based testing the test cases are derived from a model of the system under test. In our approach the model is an automaton model that is automatically extracted from the C-source code of the system under test. Beside random test data generation the test case generation uses formal methods, in detail model checking techniques. To find appropriate test cases we use the requirements defined in the system specification. To cover further execution paths we developed an additional, to our best knowledge, novel method based on special structural coverage criteria. We present preliminary results on the model extraction using a concrete industrial case study from the automotive domain

The behavior of a dependable embedded system is affected by many factors. The verification process of such a system has to consider the platform-independent as well as the platform-specific semantics of the developed software. In this work we focus on the differentiation of the platformdependent and platform-specific characteristics of a system under test and present a unified framework that shows the correctness of a an embedded system in two steps: First we verify the platform-independent semantics by showing that the system under test conforms to the specification. This is done by means of formal verification. Secondly we prove if the platform-specific semantics of the system on the target platform still conforms to the requirements defined in the specification. This step is realized by applying automatically generated test cases to the system under test on the target platform.

Due to the increasing usage of control sys- tems in cars (e.g., ESP, steer-by-wire, brake-by-wire), the fact, that more and more applications are also classified as safety- critical, for instance according to the safety standard IEC 61508 (1), and the increasing complexity of software, there is a strong need to improve the testing processes within the auto- motive domain to ensure the quality of the developed systems. We introduce the development of a testing framework using for- mal methods. The test cases are automatically derived from a model of the system under test based on the requirements defined in the system specification. This is done by means of model checking. Also the evaluation of the testing results is automated to meet test quality criteria, e.g., coverage metrics. I. MODEL-BASED TESTING Our testing framework is based on the concepts of model- based testing (2). In model-based testing the test cases are derived from a model of the system under test (SUT). The resulting test cases are applied to the system under test (Fig.1).