Японская корпорация JTEKT, производитель систем усиления рулевого управления, выбрала язык программирования SPARK и инструментальные средства компании AdaCore для разработки и верификации критического для безопасности ПО, сертифицируемого по стандарту ISO 26262. В автономных транспортных средствах система рулевого управления должна взаимодействовать с другими системами, например с системой контроля полосы движения, и ее программное обеспечение имеет наивысший уровень критичности для безопасности – ASIL D (Automotive Safety Integrity Level) стандарта ISO 26262. Тестирование ПО показывает ...