Компания AbsInt GmbH, производитель средств статического анализа программного обеспечения критически важных для безопасности встраиваемых систем, объявила об интеграции компанией Robert Bosch GmbH продуктов AbsInt в процессы разработки и верификации ПО автомобильных систем Bosch, в частности, систем рулевого управления. Компания Robert Bosch применяет два статических анализатора AbsInt: Astree — анализатор C-программ на отсутствие динамических (run-time) ошибок и состязаний за данные и RuleChecker — контроллер нормативов кодирования и сбора метрик программного кода на языке С. Оба анализатора используются Bosch по глобальной (worldwide) лицензии с правом использования в любом подразделении в мире.
Анализатор Astree исследует текст программы и обнаруживает потенциальные ошибки времени исполнения (run-time): деление на ноль, выход индекса массива за пределы, нулевые, неинициализированные и повисшие указатели, арифметические переполнения (целочисленные и с плавающей точкой), чтение неинициализированных переменных, состязания за данные при доступе из параллельно исполняющихся потоков, некорректные вызовы стандартных системных сервисов ARINC 653, OSEK и AUTOSAR и другие программные дефекты, способные привести к нарушению функциональной безопасности (safety) и информационной безопасности (security). Анализирует сотни тысяч строк программного кода за десятки минут без «ложных тревог». Используется более 10 лет в авиационных и космических проектах, автомобильной промышленности и атомной энергетике. Анализатор RuleChecker поддерживает стандарты: MISRA C:2004, MISRA C:2012, MISRA C:2012 Amendment 1, ISO/IEC TS 17961:2013, SEI CERT Secure C и MITRE CWE (Common Weakness Enumeration). Все анализаторы AbsInt cопровождаются пакетом поддержки квалификации QSK (Qualification Support Kit) для сертификации по стандартам безопасности программного обеспечения ISO 26262, DO-178C, EN 50128 и др.
Другие продукты компании AbsInt : aiT – статический анализатор времени исполнения наихудшего случая WCET (Worst Case Execution Time) ПО одноядерных процессоров; TimeWeaver — анализатор времени исполнения наихудшего случая WCET ПО многоядерных процессоров; StackAnalyzer – статический анализатор размера используемого стека для доказательства отсутствия ситуаций переполнения стека; CompCert – формально верифицированный оптимизирующий С компилятор.
Анализаторы компании AbsInt разработаны с использованием математического аппарата Абстрактной Интерпретации (Abstract Interpretation), отсюда и название компании. Все продукты AbsInt доступны для 30-дневного тест-драйва. Дистрибьютор компании AbsInt в России – компания АВД Системы, поставщик средств разработки программного обеспечения критически важных для безопасности сертифицируемых встраиваемых компьютерных систем.
