Абсент
 | Эта статья могла быть создана или отредактирована в обмен на нераскрытые платежи Википедии , что является нарушением условий использования . Может потребоваться очистка в соответствии с политикой Википедии в отношении контента , особенно с нейтральной точки зрения . ( март 2021 г. ) |
 | |
| Тип компании | Общество с ограниченной ответственностью |
|---|---|
| Промышленность | Инструменты проверки программного обеспечения |
| Основан | 1998 год |
| Штаб-квартира | , |
Ключевые люди | Основатели: Кристиан Фердинанд, Даниэль Кестнер, Марк Лангенбах, Флориан Мартин, Стефан Тезинг и Рейнхард Вильгельм. |
| Продукты | aiT, StackAnalyzer, Astrée, RuleChecker, CompCert, TimingProfiler, TimeWeaver |
| Веб-сайт | www |
AbsInt — поставщик инструментов для разработки программного обеспечения, базирующийся в Саарбрюккене , Германия . Компания была основана в 1998 году как технологическое отделение кафедры языков программирования и построения компиляторов профессора Рейнхарда Вильгельма Саарского университета . AbsInt специализируется на инструментах проверки программного обеспечения, основанных на абстрактной интерпретации . [1] Его инструменты используются по всему миру компаниями из списка Fortune 500, образовательными учреждениями, государственными учреждениями и стартапами.
Продукты
[ редактировать ]Анализатор aiT WCET статически вычисляет безопасные верхние границы для времени выполнения в наихудшем случае. [2] задач в системах реального времени . Он напрямую анализирует двоичные исполняемые файлы и учитывает поведение встроенного кэша и конвейера микропроцессора. [3] США Национальное управление безопасности дорожного движения (NHTSA) и НАСА использовали его в своем исследовании внезапного непреднамеренного ускорения в электронных системах управления дроссельной заслонкой автомобилей Toyota. [4]
StackAnalyzer определяет максимальное использование стека задачами во встроенных приложениях и может доказать отсутствие переполнения стека . Результаты анализа действительны для всех входов и каждого выполнения задачи. [5] StackAnalyzer используется в аэрокосмической, медицинской, телекоммуникационной и транспортной отраслях.
Astrée — статический анализатор программ, который доказывает отсутствие ошибок во время выполнения критически важных для безопасности встроенных приложений, написанных или автоматически генерируемых C. на [6] Он используется в оборонной/аэрокосмической, медицинской, промышленной контрольной, электронной, телекоммуникационной/информационной отраслях и на транспорте. Astrée создана группой Патрика Кузо из CNRS / ENS и разрабатывается и распространяется AbsInt по лицензии CNRS/ENS. На 6-й выставке инструментов статического анализа (SATE VI) [7] NIST (2020), было подтверждено , что Астре соответствует критериям звукового анализа SATE VI Ockham. [8]
RuleChecker — это статический анализатор программ, который автоматически проверяет код C/C++ на соответствие рекомендациям по кодированию, включая MISRA C /C++, SEI CERT C , CWE , ISO/IEC TS 17961:2013 и Adaptive Autosar C++ Coding Guidelines.
TimeWeaver — это гибридный инструмент анализа WCET , который сочетает в себе статический анализ пути и статический анализ значений с ненавязчивой трассировкой на уровне инструкций в реальном времени для ограничения времени выполнения в наихудшем случае ( WCET ). Этот подход работает для широкого спектра современных высокопроизводительных ( многоядерных ) процессоров.
CompCert — официально проверенный оптимизирующий компилятор C. Его предполагаемое использование — компиляция критически важного для безопасности и критически важного программного обеспечения, написанного на C и отвечающего высоким уровням безопасности. Он создает машинный код для архитектур PowerPC, ARM и AArch64, IA32 (32-разрядная версия x86), AMD64 и RISC-V (32- и 64-разрядная версия). С 2015 года AbsInt предлагает коммерческие лицензии, обеспечивает поддержку и обслуживание промышленного уровня, а также способствует развитию инструмента. За разработку CompCert Ксавье Лерой и команда разработчиков CompCert получили премию ACM Software System Award 2021 .
История
[ редактировать ]AbsInt — это отделение 1998 года кафедры языков программирования и компиляторов Саарского университета , где его основатели разработали общую и генеративную структуру для статических анализаторов и оптимизаторов программ на двоичном уровне. Важным компонентом этой структуры является генератор программных анализаторов PAG, который позволяет автоматически генерировать статические анализаторы на основе математической спецификации абстрактных областей и передаточных функций. [9] Первая версия PAG была выпущена в 1995 году. Вместе с PAG/WWW доступна бесплатная академическая версия PAG, которая использовалась во всем мире на многочисленных учебных курсах.
В 2001 году была запущена линейка продуктов StackAnalyzer для статического анализа использования стека , а в 2002 году — линейка продуктов aiT WCET Analyzer. В 2004 году, всего через полгода после запуска, aiT была удостоена Премии Европейского информационного общества в области технологий. [10] за «новаторские продукты, которые представляют собой лучшее из европейских инноваций в технологиях информационного общества». В 2004 году aiT использовался для анализа программного обеспечения управления полетом Airbus A380, крупнейшего в мире пассажирского самолета. [11] В 2006 году анализаторы успешно прошли первый конкурс WCET Tool Challenge, организованный Университетом Мелардалена (цитата). В 2010 году aiT и StackAnalyzer были интегрированы в SCADE Suite от Esterel Technologies , что сделало его первой в мире средой разработки встроенного программного обеспечения, в которой реализованы WCET и анализ стека на уровне модели. [12]
Разработка Astrée началась с нуля в ноябре 2001 года профессором Патриком Кузо в Лаборатории информатики Высшей нормальной школы (LIENS) при первоначальной поддержке проекта ASTRÉE, Национального центра научных исследований, Высшей нормальной школы и , с сентября 2007 года, компания INRIA (Париж-Рокенкур). Astrée означает встроенный программный статический анализатор в реальном времени . Он успешно использовался в программном обеспечении управления полетом самолетов AIRBUS A340 и A380. [13] где он не вызывал ложных тревог, даже при сложных вычислениях с числами с плавающей запятой. В апреле 2008 года Астре удалось доказать отсутствие каких-либо ошибок во время выполнения в версии C программного обеспечения автоматической стыковки автоматического транспортного средства (ATV) Жюля Верна , используемого для транспортировки полезных грузов на Международную космическую станцию . [14] С 2009 года Astrée коммерчески доступен от AbsInt по лицензии ENS/CNRS.
AbsInt участвовал во многих исследовательских проектах, финансируемых Европейской комиссией и Министерством образования и исследований Германии , таких как DAEDALUS, ARTIST, SuReal, ASTEC, ALL-TIMES, Interested, Verisoft, PREDATOR, TIMMO2USE, MBAT и других.
Название AbsInt происходит от абстрактной интерпретации — методологии статического анализа программ, основанной на семантике . [15]
Ссылки
[ редактировать ]- ^ Кестнер, Д.; Фердинанд, К. (2011). Эффективная проверка нефункциональных свойств безопасности путем абстрактной интерпретации: время, потребление стека и отсутствие ошибок времени выполнения . Материалы 29-й Международной конференции по системной безопасности ISSC2011, Лас-Вегас.
- ^ Вильгельм, Рейнхард; Энгблом, Якоб; Эрмедаль, Андреас; Холсти, Никлас; Тезинг, Стефан; Уолли, Дэвид; Бернат, Гиллем; Фердинанд, Кристиан; Хекманн, Рейнхольд; Митра, Тулика; Мюллер, Франк; Пуаут, Изабель; Пушнер, Питер; Сташулат, Ян; Стенстрем, Пер (2008). «Проблема времени выполнения в наихудшем случае — обзор методов и обзор инструментов». Транзакции ACM во встроенных вычислительных системах . 7 (3): 1–53. CiteSeerX 10.1.1.458.3540 . дои : 10.1145/1347375.1347389 . S2CID 2139310 .
- ^ Фердинанд, Кристиан; Вильгельм, Рейнхард (1999). «Быстрое и эффективное прогнозирование поведения кэша для систем реального времени». Системы реального времени . 17 (2–3): 131–181. дои : 10.1023/а:1008186323068 . S2CID 28282721 .
- ^ НАСА (18 января 2011 г.). Техническая поддержка Национальной администрации безопасности дорожного движения (NHTSA) по заявленному расследованию непреднамеренного ускорения (UA) Toyota Motor Corporation (TMC) (технический отчет). п. 151.
- ^ Фердинанд, Кристиан; Хекманн, Рейнхольд (2007). «Статическая память и анализ времени выполнения встроенного кода». Журнал транзакций легковых автомобилей SAE 2006 — электронные и электрические системы . Серия технических документов SAE. 9 . дои : 10.4271/2006-01-1499 .
- ^ Кестнер, Д.; Вильгельм, С.; и др. (2010). Астре: Доказательство отсутствия ошибок времени выполнения . Конгресс по встроенному программному обеспечению и системам реального времени ERTS², Тулуза.
- ^ SATE VI Критерии звукового анализа Оккама
- ^ Блэк, Пол; Валия, Канвардип (2020). NISTIR8304 — Критерии звукового анализа Оккама SATE VI (Отчет). Национальный институт стандартов и технологий США (NIST). doi : 10.6028/NIST.IR.8304 .
- ^ Альт, Мартин; Мартин, Флориан (1995). «Создание эффективных межпроцедурных анализаторов с помощью PAG». Материалы 2-го Международного симпозиума по статическому анализу (SAS '95) . Конспекты лекций по информатике (983): 33–50. CiteSeerX 10.1.1.37.9598 . дои : 10.1007/3-540-60360-3_31 .
- ^ ict-prize.org на сайте web.archive.org , получено 29 сентября 2023 г.
- ^ Суирис, Жан; Ле Павек, Эрван; Химберт, Гийом; Жегу, Виктор; Бориос, Гийом; Хекманн, Рейнхольд (2005). Вычисление времени выполнения программы авионики в наихудшем случае посредством абстрактной интерпретации . Материалы 5-го международного семинара по наихудшему времени исполнения (WCET '05), Майорка, Испания. стр. 21–24.
- ^ Фердинанд, К.; Хекманн, Р.; Ле Сержан, Т.; Лопес, Д.; Мартин, Б.; Форнари, X.; Мартин, Ф. (2008). Объединение средства проектирования высокого уровня для критически важных систем с инструментом для анализа WCET исполняемых файлов . 4-й Европейский конгресс ERTS — Embedded Real Time Software, Тулуза.
- ^ Дельмас, Д.; Суирис, Дж. (2007). «АСТРЭ: от исследований к промышленности». Материалы 14-го Международного форума. Симпозиум по статическому анализу (SAS'07), Конгенс Люнгбю, Дания . Конспекты лекций по информатике 4634, Springer: 437–451.
- ^ Буиссу, О.; Конке, Э.; и др. (2009). Валидация космического программного обеспечения с использованием абстрактной интерпретации . Труды 13-й конференции по системам данных в аэрокосмической отрасли, DASIA 2009, Стамбул, Турция.
- ^ Кусо, Патрик; Кузо, Радия (1977). Абстрактная интерпретация: единая решетчатая модель для статического анализа программ путем построения или аппроксимации неподвижных точек . Четвертый ежегодный симпозиум ACM SIGPLAN-SIGACT по принципам языков программирования. стр. 238–252.