Verification of embedded software models by combining abstract interpretation, symbolic execution and stability analysis

Embedded systems play an important role in many technological applications, which become increasingly complex, e.g. mobility. With higher degrees of automation, especially in domains such as automated flying or driving, the quantity and complexity of the embedded software grows significantly. Model-based design supports interdisciplinary teams to develop high quality software for embedded systems rapidly. Control design is one potential application for model-based design, so software controlled systems can be simulated and deployed from an integrated toolchain. Nevertheless, the availability of tools to verify control systems, which are deployed in industrial or research projects, remains limited. In particular, discretization and implicit side effects hardens validation when designing controllers. For example, often floating point numbers are chosen as data type without considering corner cases and rounding errors. Formally, safety in industry is measured by the compliance with a corresponding safety norm, such as IEC 61508, ISO 26262, DO-178C or others. Depending on the safety integrity level, different assessments are required. Components with increased risk must be validated with the necessary diligence. For instance, higher safety integrity levels require all execution paths to be tested. A variety of commercial tools offer automated test case generation, applying different techniques, e.g., random testing. However, concepts to generate test cases for control systems are rarely available. In this thesis, an integrated concept to validate models automatically is introduced, supporting model-based design. Instead of resolving errors at source code level or during hardware in the loop testing, our method aims to detect errors as early as possible. The presented techniques are focused on MathWorks products and include block diagrams, statecharts and MATLAB source code. However, the methods can also be applied to models from other vendors. Key findings from control theory are integrated to derive properties, easing the verification process. Our solution is manifold. First, a fitting control system description is extracted from the model. A distinction between linear, polynomial, reset, positive and uncertain systems is performed. For each type, a thorough analysis is conducted on the output boundaries and internal stability. Results are fed back into a value and slope range analysis combined with symbolic execution. Features include the incorporation of the peak-to-peak gain and invariants, which are based on Lyapunov functions. Test suits, satisfying coverage, are constructed by combining optimal control theory with a symbolic solver