Компания AdaCore завершила исследовательский проект, проведенный по заказу корпорации DENSO – крупнейшего японского производителя автомобильных комплектующих. Целью проекта было продемонстрировать применение формальных методов для выполнения требований стандарта функциональной безопасности автомобильного ПО ISO 26262 в части обеспечения «Freedom from Interference» (Свободы от Вторжений) – защиты приложений с высоким уровнем критичности для безопасности ASIL (Automotive Safety Integrity Level) от влияния сбоев, возникших в приложениях с низким уровнем критичности ASIL, унаследованных (legacy) из предыдущих проектов и написанных на языке Си.

В качестве языка программирования для разработки защищенных высококритичных приложений был применен язык SPARK, позволяющий проводить формальную верификацию – доказательство корректности работы ПО с помощью математических методов. Язык SPARK является подмножеством языка Ada - международного стандарта ISO 8652. В последней редакции стандарта ISO 8652-2012 (Ada 2012) введена конструкция для задания «контрактов» - требований к результатам работы программного модуля, описанных непосредственно в тексте программы на языке Ada. «Контракт» предназначен для использования компилятором для выполнения динамических проверок или средствами статического анализа для формальной верификации.

В этом проекте компания AdaCore выступила не только поставщиком средств формальной верификации ПО на языке SPARK, но и разработчиком методологии создания «контрактов» для обеспечения требований Freedom from Interference в ISO 26262, а также технологии «гибридной верификации» - совмещения формальных методов с традиционной верификацией ПО, основанной на тестировании.