ЭКЛЕР - ECLAIR
эта статья нужны дополнительные цитаты для проверка.Декабрь 2012 г.) (Узнайте, как и когда удалить этот шаблон сообщения) ( |
Разработчики) | БУГСЕНГ, ООО |
---|---|
Стабильный выпуск | 1.2 / 12 ноября 2012 г. |
Операционная система | Кроссплатформенность |
Тип | Статический анализ кода |
Лицензия | Проприетарный |
Интернет сайт | багшенг |
ЭКЛЕР это реклама статический анализ кода инструмент, разработанный ООО «БУГСЕНГ» для автоматического анализа, проверки, тестирования и преобразования C и C ++ программы.
Возможности
ECLAIR - это полная модернизация серии прототипов.[1] разработан в Лаборатории прикладных формальных методов Университет Пармы. Оно использует формальные методы методы статического анализа кода, такие как абстрактная интерпретация и проверка модели в сочетании с удовлетворение ограничений методы обнаружения или доказательства отсутствия определенных ошибки времени выполнения в исходный код, и обеспечивает поддержку для анализа и проверки программ, создания тестов программ и преобразования программ.
Что касается анализа и проверки программ, ECLAIR может статически обнаруживать или подтверждать отсутствие аномалий времени выполнения, а также автоматически проверять соответствие нескольким стандартам кодирования, таким как MISRA C, MISRA C ++, Стандарт безопасного кодирования CERT C, Стандарт безопасного кодирования CERT C ++,[2] C ++ с высокой степенью интеграции, НАСА /JPL C, ЕКА / BSSC C / C ++, JSF C ++, EC--,[3] Встроенный Netrino C,[4] Сила десяти (С),[5] Промышленная сила C ++.[6]
Для тестирования программы ECLAIR может автоматически синтезировать наборы входных данных модульного тестирования, которые достигают указанного пользователем критерия покрытия, предупреждая пользователя, когда из-за недопустимых условий в программе это покрытие не может быть достигнуто.
Что касается преобразования программы, ECLAIR может использоваться для выполнения сложных преобразований программы: они определяются синтаксическими и семантическими критериями; программные области в источнике, которые соответствуют этим критериям, могут быть при желании заменены параметризованной заменой.
Смотрите также
- Абстрактная интерпретация
- Проверка модели
- Статический анализ кода
- Список инструментов для статического анализа кода
использованная литература
- ^ Р. Багнара; П. М. Хилл; Э. Заффанелла (2007). "Среда на основе Пролога для рассуждений о языках программирования". arXiv:0711.0345 [cs.PL ].
- ^ Сикорд, Роберт С. (2013). Безопасное кодирование на C и C ++. Серия SEI в программной инженерии (2-е изд.). Эддисон-Уэсли Профессионал. ISBN 978-0-321-82213-0.
- ^ Хаттон, Л. (2005). «EC - более безопасное подмножество ISO C на основе измерений, подходящее для разработки встроенных систем». Информационные и программные технологии. 47 (3): 181–695. CiteSeerX 10.1.1.101.7828. Дои:10.1016 / j.infsof.2004.08.001.
- ^ Барр, Майкл (2008). Встроенный стандарт кодирования C. Barr Group. ISBN 978-1442164826.
- ^ Джеральд, Дж. (2006). «Сила 10: правила разработки критически важных для безопасности кодексов». Компьютер. 39 (6): 95–97. Дои:10.1109 / MC.2006.212.
- ^ Хенриксон, Матс; Найквист, Эрик (1997). Промышленная сила C ++. Prentice-Hall PTR. ISBN 978-0131209657.