Safety Verification Method for Priority-Based Real-Time Software

摘要

The number of functions and the sizes of electronic controls and software systems in automobiles are increasing, as ADAS and autonomous driving systems are realized. A higher safety level is also being demanded for complex control systems, so functional safety standards, such as ISO 26262, are increasingly being introduced to in-vehicle systems. In safety-critical systems, failures are diagnosed by the cooperative function of hardware and software. Furthermore, the diagnostic software consists of a mixture of a cyclic execution portion and a hardware-event-driven portion. Testing the cooperative function of multiple concurrent processes is impractically time consuming because the combinations of conditions are so numerous. Formal verification technology is effective because it enables exhaustive verification of a vast quantity of test cases including unexpected states, but a modeling methodology for timing-related uncertainty between hardware events and cyclic software executions has not been established. Our proposed method is to model a combination of the concurrent executions of multiple tasks under non-deterministic event from hardware. We chose the C-language-based model checker CBMC as a verification engine and made an extension to CSeq as a concurrency pre-processor. We proposed the common verification architecture for functional safety software and developed priority-based scheduling mechanism and the event-injection mechanism on CSeq.