AbsInt - Википедия - AbsInt

AbsInt Angewandte Informatik GmbH
ТипGesellschaft mit beschränkter Haftung
ПромышленностьИнструменты проверки программного обеспечения
Основан1998; 22 года назад (1998)
Штаб-квартира
Саарбрюккен
,
Германия
Ключевые люди
Основатели: Кристиан Фердинанд, Даниэль Кестнер, Марк Лангенбах, Флориан Мартин, Стефан Тезинг и Райнхард Вильгельм
ТоварыaiT, StackAnalyzer, Astrée, RuleChecker, CompCert, TimingProfiler, TimeWeaver
Интернет сайтwww.absint.com

AbsInt является поставщиком инструментов для разработки программного обеспечения, базирующимся в Саарбрюккен, Германия. Компания была основана в 1998 году как технологическое подразделение отдела языков программирования и создания компиляторов. Проф. Райнхард Вильгельм в Саарский университет. AbsInt специализируется на инструментах проверки программного обеспечения на основе абстрактная интерпретация.[1] Его инструменты используются во всем мире компаниями из списка Fortune 500, образовательными учреждениями, государственными учреждениями и стартапами.

Товары

aiT WCET Analyzer статически вычисляет безопасные верхние границы для время исполнения в наихудшем случае[2] задач в системы реального времени. Он непосредственно анализирует двоичные исполняемые файлы и принимает во внимание внутренний кэш и поведение микропроцессора.[3] Соединенные штаты. Национальная администрация безопасности дорожного движения (НАБДД) и НАСА использовал его в Исследование внезапного непреднамеренного ускорения в электронных системах управления дроссельной заслонкой автомобилей Toyota.[4]

StackAnalyzer определяет максимальное использование стека задачами во встроенных приложениях и может доказать отсутствие переполнение стека. Результаты анализа действительны для всех входов и каждого выполнения задачи.[5] StackAnalyzer используется в аэрокосмической, медицинской, телекоммуникационной и транспортной отраслях.

Astrée статический анализатор программ, который доказывает отсутствие ошибок времени выполнения в критически важных для безопасности встроенных приложениях, написанных или автоматически созданных на C.[6] Он используется в оборонной / аэрокосмической, медицинской, производственной, электронной, телекоммуникационной / цифровой и транспортной отраслях. Astrée происходит из группы Патрик Кузо в CNRS /ENS и разрабатывается и распространяется AbsInt по лицензии CNRS / ENS.

RuleChecker - это статический анализатор программ, который автоматически проверяет код C / C ++ на соответствие рекомендациям по кодированию, включая MISRA C / C ++, SEI CERT C, CWE, ISO / IEC TS 17961: 2013 и Рекомендации по кодированию Adaptive Autosar C ++.

TimeWeaver - это гибрид WCET инструмент анализа, который сочетает статический анализ пути и статический анализ значений с ненавязчивой трассировкой на уровне инструкций в реальном времени, чтобы ограничить время выполнения наихудшего случая (WCET ). Такой подход работает для широкого спектра современных высокопроизводительных (многоядерный ) процессоры.

CompCert - это официально проверенный оптимизирующий компилятор C. Его предполагаемое использование - это компиляция критически важного для безопасности и критически важного программного обеспечения, написанного на C и отвечающего высоким уровням гарантии. Он производит машинный код для архитектур PowerPC (32-бит), ARM и IA32 (x86 32-бит). С 2015 года AbsInt предлагает коммерческие лицензии, обеспечивает техническую поддержку и обслуживание, а также вносит свой вклад в развитие инструмента.

История

AbsInt - это дочернее предприятие 1998 года факультета языков программирования и компиляторов Саарский университет, где его основатели разработали общую и генерирующую структуру для статических анализаторов и оптимизаторов программ двоичного уровня. Важным компонентом этой структуры является Program Analyzer Generator PAG, которая позволяет автоматически генерировать статические анализаторы из математической спецификации абстрактных областей и передаточных функций.[7] Первая версия PAG была выпущена в 1995 году. Вместе с PAG / WWW доступна бесплатная академическая версия PAG, которая использовалась во всем мире в многочисленных учебных курсах.

В 2001 году линейка продуктов StackAnalyzer для статического использование стека был запущен анализ, а в 2002 году - линейка продуктов aiT WCET Analyzer. В 2003 году, всего через полгода после запуска, компания aiT была удостоена Европейской премии в области технологий информационного общества за «новаторские продукты, представляющие лучшие европейские инновации в технологиях информационного общества. ". В 2004 году aiT использовался для анализа программного обеспечения управления полетом Airbus A380, крупнейшего в мире пассажирского самолета.[8] В 2006 году «Анализаторы» успешно прошли первый WCET Tool Challenge проведено Университетом Мелардален (ссылка). В 2010 году aiT и StackAnalyzer были интегрированы в SCADE Suite из Эстерель Технологии, что делает его первой в мире средой разработки встроенного программного обеспечения, в которой реализован WCET и стек-анализ на уровне модели.[9]

Разработка Astrée началась с нуля в ноябре 2001 г. проф. Патрик Кузо в Лаборатории информатики Высшей школы (LIENS), первоначально поддержанной проектом ASTRÉE, Национальным центром научных исследований, Высшей школой, а с сентября 2007 г. INRIA (Париж-Роккенкур). Astrée означает Аналитик statique de logiciels temps-réel embarqués («Встроенный программный статический анализатор реального времени»). Он успешно использовался в программном обеспечении управления полетом самолетов AIRBUS A340 и A380,[10] где он не вызывал ложных срабатываний даже для сложных вычислений с числами с плавающей запятой. В апреле 2008 года Astrée смогла доказать отсутствие каких-либо ошибок времени выполнения в версии C программного обеспечения автоматической стыковки Автомат Жюля Верна (ATV) используется для перевозки грузов на Международная космическая станция.[11] С 2009 года Astrée коммерчески доступна от AbsInt по лицензии ENS / CNRS.

AbsInt участвовал во многих исследовательских проектах, финансируемых Европейская комиссия и Министерство образования и науки Германии, такие как DAEDALUS, ARTIST, SuReal, ASTEC, ALL-TIMES, заинтересованных, Verisoft, PREDATOR, TIMMO2USE, MBAT и другие.

Название AbsInt происходит от абстрактная интерпретация, основанная на семантике методология для статический анализ программы.

Рекомендации

  1. ^ Kästner, D .; Фердинанд, К. (2011). Эффективная проверка нефункциональных свойств безопасности путем абстрактной интерпретации: время, потребление стека и отсутствие ошибок времени выполнения. Материалы 29-й Международной конференции по системной безопасности ISSC2011, Лас-Вегас.
  2. ^ Вильгельм, Рейнхард; Энгблом, Якоб; Эрмедаль, Андреас; Холсти, Никлас; Тезинг, Стефан; Уолли, Дэвид; Бернат, Гиллем; Фердинанд, Кристиан; Хекманн, Райнхольд; Митра, Тулика; Мюллер, Франк; Пуаут, Изабель; Пушнер, Питер; Стащулат, Ян; Стенстрём, Пер (2008). "Проблема времени выполнения наихудшего случая - Обзор методов и обзор инструментов". Транзакции ACM во встроенных вычислительных системах. 7 (3): 1–53. CiteSeerX  10.1.1.458.3540. Дои:10.1145/1347375.1347389.
  3. ^ Фердинанд, Кристиан; Вильгельм, Рейнхард (1999). «Быстрое и эффективное прогнозирование поведения кеша для систем реального времени». Системы реального времени. 17 (2–3): 131–181. Дои:10.1023 / а: 1008186323068.
  4. ^ НАСА (18 января 2011 г.). Техническая поддержка Национальной администрации безопасности дорожного движения (NHTSA) в расследовании заявленного Toyota Motor Corporation (TMC) непреднамеренного ускорения (UA) (Технический отчет). п. 151.
  5. ^ Фердинанд, Кристиан; Хекманн, Райнхольд (2007). «Статическая память и анализ времени выполнения встроенного кода». Журнал транзакций легковых автомобилей SAE 2006 - Электронные и электрические системы. Серия технических статей SAE. 9. Дои:10.4271/2006-01-1499.
  6. ^ Kästner, D .; Wilhelm, S .; и другие. (2010). Астре: Доказательство отсутствия ошибок времени выполнения. Конгресс по встроенному программному обеспечению и системам реального времени ERTS², Тулуза.
  7. ^ Альт, Мартин; Мартин, Флориан (1995). «Создание эффективных межпроцедурных анализаторов с ПАГ». Материалы 2-го Международного симпозиума по статическому анализу (SAS '95). Конспект лекций по информатике (983): 33–50. CiteSeerX  10.1.1.37.9598. Дои:10.1007/3-540-60360-3_31.
  8. ^ Суйрис, Жан; Ле Павец, Эрван; Химбер, Гийом; Джегу, Виктор; Бориос, Гийом; Хекманн, Райнхольд (2005). Вычисление времени выполнения программы авионики в наихудшем случае путем абстрактной интерпретации. Труды 5-го Международного семинара по времени исполнения наихудшего случая (WCET '05), Майорка, Испания. С. 21–24.
  9. ^ Фердинанд, К .; Heckmann, R .; Le Sergent, T .; Lopes, D .; Martin, B .; Форнари, X .; Мартин, Ф. (2008). Сочетание инструмента проектирования высокого уровня для критически важных для безопасности систем с инструментом для анализа WCET исполняемых файлов. 4-й Европейский конгресс ERTS - Встроенное программное обеспечение реального времени, Тулуза.
  10. ^ Delmas, D .; Суйрис, Дж. (2007). «ASTRÉE: от исследований к промышленности». Материалы 14-го Междунар. Симпозиум по статическому анализу (SAS'07), Kongens Lyngby, Дания. Конспект лекций по информатике 4634, Springer: 437–451.
  11. ^ Bouissou, O .; Conquet, E .; и другие. (2009). Валидация космического программного обеспечения с использованием абстрактной интерпретации. Труды 13-й конференции по информационным системам в аэрокосмической отрасли, DASIA 2009, Стамбул, Турция.

внешняя ссылка