Calibration parameters are extensively used in complex automotive Engine Control Units (ECUs), including ECUs for the engine, transmission, Anti-lock Braking System (ABS), and Electronic Stability Control (ESC). Calibration engineers can set the exact values of calibration parameters for a given software application after the ECU software is built. Such parameters also enable a single set of software to control multiple hardware variants, for example 4-cylinder and 6-cylinder engine variants, or turbo and non-turbo variants. In an ECU, there are often hundreds and sometimes tens of thousands of calibration parameters, some of which are multidimensional tables. With this level of complexity, ensuring that the ECU software using the values from these tables will not encounter an overflow operation, divide by zero condition, or illegal memory access run-time error can be a significant challenge. Due to the connection between hardware and software, such errors could potentially cause hardware damage or unexpected behavior, which in turn can lead to end-user safety concerns
With traditional testing it is impossible to exhaustively test such complex software systems, comprised of both calibration parameters and code, to prove that the software is free of run-time errors. Verification based on formal methods may provide a means by which it may be possible to learn more about the quality of the software from a run-time perspective. With formal methods, it is possible to exhaustively verify the software, even software with sophisticated calibration parameters. Using formal methods, engineers can specify the full range of data in the calibration tables and exhaustively verify the software, rather than testing with a limited range of data in the tables.