The number of functions and the sizes of electronic controls and software systems in automobiles are increasing, as ADAS
Advanced Driver Assistance Systems
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 Clanguage-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.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 firstname.lastname@example.org
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 email@example.com