Unlike for conventional compilers for imperative programming languages such as C or ADA, no established methods for safeguarding artifacts generated by model-based code generators exist despite progress in the field of formal verification. Several test approaches dominate the engineering practice. This paper describes a general and tool-independent test architecture for code generators used in model-based development. We evaluate the effectiveness of our test approach by means of testing optimizations performed by the TargetLink code generator, a widely accepted and complex development tool used in automotive model-based development.

Mathematical modeling, which already is established for a long time in many engineering domains, now also gains strongly in importance in the development of embedded software. In the automotive sector (Schauffele and Zurawka, 2003), modeling is used on the one hand for the conceptual anticipation of the functionality to be realized (open/closed loop control, monitoring) and, on the other, for the simulation of the behavior of real physical systems (plant, environment)

This paper presents a novel testing approach for model-based design tools, termed GraphOTK, and applies it to the optimizing component of a code generator for Simulink and Stateflow models.

In model-based development, executable specifications (models) are used for the design of the software to be developed. New techniques allow the automatic generation of compact code directly from the model via so-called code generators. However, at present, code generators do not possess the same quality characteristics as C or ADA compilers which have been proven in use. The use of test suites, which make it possible to check compilers systematically, is also a promising approach for code generators. This paper describes the design of such a test suite for code generators, and introduces a new testing approach for code generator transformations.

This paper introduces a dual approach for describing the software of embedded systems in motor vehicles. The approach divides the description into two parts, an operational model and a number of associated model properties. Starting from a tool-based software design with established structured methods that are basically suitable for the integration of mathematically precise techniques, proposals are made for the selective integration of formal methods into the description of properties of design components. By systematically checking these two views against each other it is possible to detect and eliminate inconsistencies and errors in the modelling at an early stage of development. The presented approach aims at applying the advantages of a more formal approach to the development of automotive software in an industrial setting. For evaluation purposes, the presented concepts are applied to the software of a cruise control system.

Software testing often consumes up to 50 percent of the overall software costs. A large amount of time and money within the test process is spent due to incomplete, inconsistent or ambiguous informal specifications of the test objects. A more formal approach to the early phases of software development can reduce the error rate drastically and in addition, can significantly improve the central testing activities like test case design and test evaluation. This paper presents an approach for generating test cases from formal specifications written in Z by combining the classification-tree method for partition testing with the disjunctive normal form approach. Firstly, a classification tree describing high level test cases is constructed from the formal specification of the test object. Then the high level test cases are further refined by generating a disjunctive normal form for them. The refined test cases obtained this way cover all specified aspects of the system explicitly and also contain all information necessary to evaluate the test results. The proposed combination of the classification-tree method with the disjunctive normal form approach preserves advantages of both methods, overcomes most of their limitations, and can be supported by tools.