Должен ли я использовать автоматизированные средства проверки?

Question

Мне интересно доказать, что некоторый контроллер робота не достигает какого-либо неисправного состояния, которое я определил бы с помощью набора предикатов. Я знаю, что для этого есть программные средства с открытым исходным кодом. Например, я слышал о BLAST (инструмент проверки программного обеспечения Berkeley Lazy Abstraction), но знаете ли вы о каком-либо другом, который может быть проще в использовании и / или более ориентирован на мое конкретное приложение?

Вы когда-нибудь использовали BLAST или другой подобный инструмент в одном из своих проектов, и считаете ли вы, что преимущества перевешивают усилия, необходимые для развертывания таких инструментов?

Answer 1

Может оказаться полезным Frama-C .

Оценки, выполненные людьми, не являющимися разработчиками Frama-C, см. в этих двух статьях .Некоторые инженеры, разрабатывающие код, критичный для безопасности (например, DO-178B уровня A), нашли формальные аннотации и анализ, основанные на самых слабых методах предварительных условий , которые стоят инвестиций , но традиционные тесты для них очень дороги.Эта последняя ссылка о Caveat, анализаторе с закрытым исходным кодом, который Frama-C намеревается заменить в свое время.

Ваш вопрос звучит так, как будто вы, возможно, оцените Frama-C Aoraï плагин.

Является ли это все время, проведенное в вашем случае, вероятно, больше зависит от того, считаете ли вы изучение этих методов радостью или делом.