Fluctuat - Fluctuat

Fluctuat
Разработчики)Commissariat à l'Énergie Atomique
Написано вC ++
Операционная система
Доступно ванглийский
ТипФормальная проверка, Статический анализ кода
ЛицензияКоммерческий
Интернет сайтwww.lix.polytechnique.fr/ Labo/ Сильви.Putot/ флуктуат.html

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

Теоретические основы

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

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

х = [0,1]; у = 2 * х + 1; z = х * у;

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

особенности

Возможности Fluctuat включают:

Смотрите также

использованная литература

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

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