Search Results

Software developers in the automotive sector must achieve high quality objectives. Many design and implementation errors are avoided by synthesizing code from model-based software specifications using automatic code generators such as ETAS' ASCET. To verify non-functional properties of the implementation, model-based design processes should be complemented with static program analysis tools like AbsInt's StackAnalyzer and timing analyzer aiT. ASCET, StackAnalyzer and aiT can be integrated in a way that the analysis results for code generated by ASCET are conveniently accessible from within the ASCET development environment. This gives ASCET users a direct feedback on the effects of their design decisions on resource usage, allowing to select more efficient designs and implementation methods. In the paper, we present the tools, the experimental integration, preliminary results and plans for further tool integration.

Developers of safety-critical real-time systems have to ensure that their systems react within given time bounds. Ideally, the system is designed to provide sufficient computing power and network bandwidth, is cost efficient and provides the necessary safety level. To achieve this goal, three challenges have to be addressed. First, it must be possible to account for timing during early development stages in the architecture exploration phase. Second, during software development, timing behavior and the effects of software changes on timing must be observable. Third, there must be a technology for formally verifying the final timing behavior for industry-size applications. In this article we present a comprehensive methodology for dealing with timing which addresses all three issues based on state-of-the-art commercial tools.

Model-based development is the established way of developing embedded control algorithms, especially for safety-critical applications. The aim is to improve development efficiency and safety by developing the software at a high abstraction level (the model) and by generating the implementation (the C code) automatically from the model. Although model-based development focuses on the models themselves, downstream artifacts such as source code or executable object code have to be considered in the verification stage. Safety standards such as ISO 26262 require upper bounds to be determined for the required storage space or the execution time of real-time tasks, and the absence of run-time errors to be demonstrated. Static analysis tools are available which work at the code level and can prove the absence of such errors. However, the connection to the model level has to be explicitly established.

Failure of a safety-critical application on an embedded processor can lead to severe damage or even loss of life. Here we are concerned with two kinds of failure: stack overflow, which usually leads to run-time errors that are difficult to diagnose, and failure to meet deadlines, which is catastrophical for systems with hard real-time characteristics. Classical validation methods like code review and testing with repeated measurements require a lot of effort, are expensive, and do not really help in proving the absence of such errors. AbsInt's tools StackAnalyzer and aiT (timing analyzer) provide a solution to this problem. They use abstract interpretation as a formal method that allows to obtain statements valid for all program runs with all inputs.