Астре (статический анализ)

Астрея
Оригинальный автор(ы)	Патрик Кузо, Радия Кузо, Жером Фере, Антуан Мине, Ксавье Риваль
Разработчик(и)	Лаборатория компьютерных наук Высшей нормальной школы (Париж) (ССЫЛКИ) ; Французский институт исследований в области компьютерных наук и автоматизации (INRIA, Париж-Рокенкур)
Первоначальный выпуск	16 декабря 2002 г .; 21 год назад
Стабильная версия	23.10 / 2023 ; 1 год назад
Написано в	OCaml
Операционная система	Windows 10 , 64-разрядная версия Linux , macOS
Платформа	х86-64 ; AArch64 ( M1 , M2 , M3 )
Доступно в	Английский
Тип	статический анализатор
Лицензия	Собственный
Веб-сайт	www .астри . нас .fr

Астре ( анализатор « Статический обеспечения реального времени встроенного » программного ^{[ 1 ]}) — статический анализатор, основанный на абстрактной интерпретации . Он анализирует программы, написанные на языках программирования C и C++ , и выдает исчерпывающий список возможных ошибок времени выполнения и утверждений нарушений . Охватываемые классы дефектов включают деление на ноль , переполнение буфера , разыменование нулевых или висячих указателей , гонки данных , взаимоблокировки и т. д. Astrée включает статическую проверку на наличие ошибок и помогает находить уязвимости кибербезопасности , такие как Spectre . Это проприетарное программное обеспечение, написанное на языке OCaml .

используются специальные методы анализа Инструмент адаптирован для встроенного кода, критичного к безопасности: для общих конструкций теории управления ( конечные автоматы , цифровые фильтры , ограничители скорости...) и с плавающей запятой чисел .

Параллельный код анализируется с помощью разумной семантики чередования, которая учитывает параллельные потоки выполнения , их приоритеты и механизмы синхронизации . Astrée поддерживает модели исполнения ARINC 653 , OSEK и AUTOSAR и может быть адаптирована к дополнительным операционной системы спецификациям (ОС). На многоядерных процессорах размещение потоков по ядрам, а также использование мьютексных и спин-блокировок анализируется .

Astrée был разработан группой Патрика Кузо в École Normale Supérieure , совместной группе с CNRS , и доступен на коммерческой основе от AbsInt GmbH. Он используется в оборонно-космической промышленности, промышленном управлении, электронной и автомобильной промышленности. Одним из основных промышленных пользователей является Airbus . ^{[ 2 ]}

См. также

Список инструментов для статического анализа кода

Библиография

Брюно Бланше, Патрик Кузо, Радия Кузо, Жером Фере, Лоран Моборн, Антуан Мине, Давид Моннио и Ксавье Риваль. Проектирование и внедрение специального статического программного анализатора для критически важного для безопасности встраиваемого программного обеспечения реального времени , приглашенная глава. В сущности вычислений: сложность, анализ, преобразование. Очерки, посвященные Нилу Д. Джонсу , Т. Могенсену, Д. А. Шмидту и И. Х. Садборо (редакторы). Том 2566 конспектов лекций по информатике, стр. 85–108, Springer. дои : 10.1007/3-540-36377-7_5
Бруно Бланше, Патрик Кузо, Радия Кузо, Жером Фере, Лоран Моборн, Антуан Мине, Дэвид Моннио и Ксавье Риваль, Статический анализатор для большого программного обеспечения, критически важного для безопасности. , В PLDI 2003 — Конференция ACM SIGPLAN SIGSOFT по проектированию и реализации языков программирования, Конференция по исследованию федеративных вычислений 2003 г., 7–14 июня 2003 г., Сан-Диего, Калифорния, США, стр. 196–207, ACM. дои : 10.1145/781131.781153
Дэвид Дельмас и Жан Суирис. Астре: от исследований к промышленности. , учеб. 14-й Международный симпозиум по статическому анализу, SAS 2007, Г. Файле и Х. Риис-Нильсон (редакторы), Конгенс Люнгби, Дания, 22–24 августа 2007 г., LNCS 4634, стр. 437–451.
Арно Ж. Вене и Майкл Р. Лоури. 2010. Статический анализ для обеспечения качества программного обеспечения: надежность, масштабируемость и адаптивность. В материалах семинара FSE/SDP «Будущее исследований в области разработки программного обеспечения» (FoSER '10). ACM, Нью-Йорк, Нью-Йорк, США, 393–396. дои : 10.1145/1882362.1882442
Жан-Луи Буланже. Статический анализ программного обеспечения: абстрактная интерпретация . ISBN 978-1-84821-320-3 . Уайли.
Даниэль Кестнер, Стефан Вильгельм, Стефана Ненова, Патрик Кузо, Радия Кузо, Жером Фере, Лоран Моборн, Антуан Мине, Ксавье Риваль. Астре: Доказательство отсутствия ошибок времени выполнения . Конгресс по встроенному программному обеспечению и системам реального времени ERTS², Тулуза, 2010 г.
А. Мини, Л. Моборн, X. Ривал, Ж. Фере, П. Кузо, Д. Кестнер, С. Вильгельм, К. Фердинанд. Вывод статического анализа на новый уровень: доказательство отсутствия ошибок во время выполнения и гонок за данными с помощью Astrée. На выставке ERTS 2016: Встроенное программное обеспечение и системы реального времени, 8-й Европейский конгресс, январь 2016 г., Тулуза, Франция.
Д. Кестнер, Л. Моборн, Н. Графе, К. Фердинанд. Расширенный статический анализ звука для обнаружения дефектов программирования, связанных с безопасностью. 8-й Международный журнал достижений в области безопасности, ISSN 1942-2636 , том. 11, нет. 1 и 2, 149–159, МАРИА, 2018.
Д. Кестнер, Б. Шмидт, М. Шлундт, Л. Моборн, С. Вильгельм, К. Фердинанд. Проанализируйте это! Звуковой статический анализ для проверки интеграции крупномасштабного автомобильного программного обеспечения. Технический документ SAE 2019-01-1246, Всемирный конгресс SAE 2019, Детройт, апрель 2019 г. дои : 10.4271/2019-01-1246

Ссылки

^ "Дом" . astree.ens.fr .
^ «Самолет, который «машет крыльями», объединил множество исследователей» . Le Monde.fr . 26 апреля 2005 г.

Внешние ссылки

[1] "Дом" . astree.ens.fr .

[2] «Самолет, который «машет крыльями», объединил множество исследователей» . Le Monde.fr . 26 апреля 2005 г.

[ 1 ]

[ 2 ]