Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску

CPAchecker является основой и инструментом для формальной верификации программного обеспечения , [1] и анализ программ , из программ C . Некоторые из его идей и концепций, например ленивая абстракция, были унаследованы от программы проверки моделей программного обеспечения BLAST . [2] CPAchecker основан на идее конфигурируемого анализа программ [3], которая представляет собой концепцию, которая позволяет выражать как проверку модели, так и анализ программы с помощью одного формализма. При выполнении CPAchecker выполняет анализ достижимости , т. Е. Проверяет , может ли потенциально быть достигнуто определенное состояние, которое нарушает заданную спецификацию.[4]

Одно из применений CPAchecker - проверка драйверов устройств Linux . [5]

Достижения [ править ]

CPAchecker занял первое место в двух категориях (общая и ControlFlowInteger) на 1-м конкурсе по верификации программного обеспечения (2012), который проводился на TACAS 2012 в Таллинне . [6]

CPAchecker занял первое место (категория в целом) во 2-м конкурсе по верификации программного обеспечения (2013 г.), который проводился на TACAS 2013 в Риме . [7]

Архитектура [ править ]

CPAchecker работает с автоматами потока управления (CFA); прежде чем данная программа на C может быть проанализирована алгоритмом CPA, она преобразуется в CFA. CFA - это ориентированный граф, ребра которого представляют либо предположения, либо назначения, а его узлы представляют собой местоположения программ.

Ссылки [ править ]

  1. ^ Официальный сайт CPAchecker: http://cpachecker.sosy-lab.org
  2. ^ Дирк Бейер и Томас А. Хензингер и Ранджит Джала и Рупак Маджумдар (2007). «Средство проверки модели программного обеспечения BLAST: приложения для разработки программного обеспечения» (PDF) . Международный журнал программных средств для передачи технологий (STTT) . 9 : 505–525. DOI : 10.1007 / s10009-007-0044-Z .
  3. ^ Дирк Бейер и Томас А. Хензингер и Грегори Теодуло (2007). «Настраиваемая проверка программного обеспечения: конкретизация конвергенции проверки моделей и программного анализа» (PDF) . Материалы 19-й Международной конференции по компьютерной проверке . Springer-Verlag, Гейдельберг. ISBN  978-3-540-73367-6.
  4. ^ Дирк Бейер и М. Эркан Керемоглу (2011). «CPAchecker: инструмент для настраиваемой проверки программного обеспечения» (PDF) . Материалы 23-й Международной конференции по компьютерной верификации . Springer-Verlag, Гейдельберг. ISBN  978-3-642-22109-5.
  5. ^ Проверка драйвера Linux: http://linuxtesting.org/project/ldv
  6. ^ Дирк Бейер (2012). «Конкурс по верификации программного обеспечения (SV-COMP)» (PDF) . Труды 18-й Международной конференции по инструментам и алгоритмам построения и анализа систем . Springer-Verlag, Гейдельберг.
  7. ^ Дирк Бейер (2013). «Второй конкурс по верификации программного обеспечения (Резюме SV-COMP 2013)» (PDF) . Труды 19-й Международной конференции по инструментам и алгоритмам построения и анализа систем . Springer-Verlag, Гейдельберг.

Внешние ссылки [ править ]

  • Официальный веб-сайт