Formal Timing Analysis and Verification of the Interrupt-driven Programs for ISO26262

Safety-critical systems refer to software systems whose operation can affect the safety of people and facilities used in the automotive industry, aerospace, and hospital health care systems. The high level of safety of software in the aforementioned fields has often drawn attention. ISO26262 has been issued for the automotive industry, which defines standards and procedures, including software level, software development standards, and software validation standards to ensure the high level of safety of software. In high-safety automotive software, a real-time safeguard requires the analysis of interrupt-driven programming. Such analysis presents a challenging and complex task because of the uncertainty of interrupts. In ISO26262, the formalized method is suggested to verify the process of software development. To achieve the verification goals defined in ISO26262, we use a formal method instead of traditional verification methods to analyze worst-case execution time. We analyze interrupt-driven programs from the perspective of timeliness and present the Interrupt Control Flow Graph (ICFG), which is used to describe the control flow of interrupt-driven programs. The execution of interrupts may largely increase the number of program states, potentially leading to state explosion, resulting in a sizable ICFG. To solve this problem, we propose an algorithm for reducing the size of ICFG. On the basis of the reduced ICFG, the worst-case execution path can be determined and thus be used to verify whether the program execution time exceeds the expected time and identify the execution path that may cause a timeout problem.