Он колеблется

Он колеблется
Разработчик(и)	Комиссия по атомной энергии
Написано в	С++
Операционная система	Microsoft Windows ; FreeBSD ; Линукс ; Мак ОС Х ;
Доступно в	Английский
Тип	Формальная проверка , Статический анализ кода
Лицензия	Коммерческий
Веб-сайт	www .шесть .политехнический .fr / Два /Сильви .Бутончики /колеблется .html

Fluctuat разрабатывается Commissariat à l'Energie Atomique et aux Energies Alternatives с 2001 года. Fluctuat позволяет выполнять статический анализ программ на C и Ada , уделяя особое внимание операциям с плавающей запятой.

Теоретическая основа

Fluctuat — статический анализатор, основанный на абстрактной интерпретации . По сравнению с аналогичными инструментами, такими как Polyspace или Astrée , он опирается на зонотопы как на абстрактную область. Это означает, что значение каждой программной переменной абстрагируется с помощью линейного выражения с символами шума (внутренние переменные, которые находятся в диапазоне [-1,1]).

Теперь рассмотрим следующую программу:

x=[0,1];
y = 2*x+1;
z = x * y;

Первая строка означает, что значение x может быть любым из [0,1]. Его можно записать как x= 0,5 + 0,5*ε , где ε — символ шума. Из второй строки следует, что y= 2 + ε ; поскольку x и y имеют один и тот же шумовой символ, эта абстрактная область является реляционной. При наличии нелинейных операций, как в третьей строке, вводятся новые символы шума. Точным символическим выражением будет z=1+1,5*ε + 0,5*ε*ε , но мы абстрагируем его как z=1,25+1,5ε+0,25η .

Функции

Возможности Fluctuate включают в себя:

статический анализ программ на C и Ada . ^[1]
анализ чувствительности программных переменных. ^[2]
поколение наихудшего случая .
интерактивный анализ.
анализ гибридных систем ^[3]

См. также

Ссылки

^ Дэвид Дельмас; и др. «На пути к промышленному использованию FLUCTUAT в программном обеспечении авионики, критически важном для безопасности». Материалы 14-го международного семинара по формальным методам для промышленных критических систем FMICS'09 . ЛНКС. Том. 5825. стр. 53–69.
^ Эрик Губо и Сильви Путо. «Статический анализ численных алгоритмов». Материалы симпозиума по статическому анализу SAS'06, Сеул . ЛНКС. Том. 4134. стр. 18–34.
^ Оливье Буиссу; и др. «HybridFluctuat: статический анализатор числовых программ в непрерывной среде». Труды компьютерной верификации CAV'09, Гренобль, Франция . ЛНКС. Том. 5649. стр. 620–626. CiteSeerX 10.1.1.216.8351 .

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

Официальный сайт

[1] Дэвид Дельмас; и др. «На пути к промышленному использованию FLUCTUAT в программном обеспечении авионики, критически важном для безопасности». Материалы 14-го международного семинара по формальным методам для промышленных критических систем FMICS'09 . ЛНКС. Том. 5825. стр. 53–69.

[2] Эрик Губо и Сильви Путо. «Статический анализ численных алгоритмов». Материалы симпозиума по статическому анализу SAS'06, Сеул . ЛНКС. Том. 4134. стр. 18–34.

[3] Оливье Буиссу; и др. «HybridFluctuat: статический анализатор числовых программ в непрерывной среде». Труды компьютерной верификации CAV'09, Гренобль, Франция . ЛНКС. Том. 5649. стр. 620–626. CiteSeerX 10.1.1.216.8351 .

[1]

[2]

[3]