JTEKT — Application of SPARK to Steering System Software Development

In this webinar, Shinya Yoneki from JTEKT introduces the use of Formal Verification Tool Suite, SPARK Pro for JTEKT's electric power steering system, along with concrete examples.

The size of the software used in automobiles is continuously increasing as autonomous driving technology is being introduced and there is a need to ensure higher safety and reliability. Therefore, it is important to achieve higher quality while adhering to the development schedule. Formal verification can be used as a development method to detect defects early in the software development process and reduce the man-hours required for testing and rework.

Key Takeaways:

• Formal verification can reduce costs by finding faults in software specifications and coding bugs early in the development.
• Formal verification is important to demonstrate the safety of software without safety mechanisms.
• SPARK is best industrially supported FM tools in the market today
• SPARK can enhance the safety of vehicle software with ISO26262 ASIL D.
• Only SPARK can be used for mass production vehicle system
• SPARK is scalable and formal verification can be applied step by step from small programs to large ones.