Каков ваш опыт проверки программных моделей?

Я только что закончил класс по проверке моделей, и большие инструменты, которые мы использовали, были Spin и SMV . В конечном итоге мы использовали их для проверки свойств при распространенных проблемах синхронизации, и я обнаружил, что SMV немного проще в использовании.

Хотя эти инструменты было интересно использовать, я думаю, что они действительно сияют, когда вы объединяете их с чем-то, что динамически накладывает ограничения на вашу программу (так что немного легче проверить 'useful' вещей о вашей программе). Мы закончили тем, что взяли фреймворк Spring WebFlow, который использует XML для записи файла типа state-machine, указывающего, какие веб-страницы могут переходить на какие другие, и используя SMV, чтобы иметь возможность выполнять проверку на этих приложениях (бесстыдный плагин здесь ).

Чтобы ответить на ваш последний вопрос, я думаю, что проверка моделей определенно полезна, но я больше склоняюсь к использованию модульного тестирования как метода, который позволяет мне чувствовать себя комфортно при поставке моего конечного продукта.

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

Мы использовали средство проверки модели Java Path Finder для проверки некоторых параметров безопасности (взаимоблокировка, состояние гонки) и временных свойств (использование линейной временной логики для их определения). Он поддерживает классические утверждения (например, NotNull) на Java (байт-код) - это для проверки модели программы.

Какой инструмент проверки модели вы использовали?

Мы использовали Java Path Finder (для академических целей). Это программное обеспечение с открытым исходным кодом, разработанное NASA изначально.

Как бы вы суммировали свой опыт w/ этой методики, в частности, при оценке ее эффективности в обеспечении более высокого качества программного обеспечения?

Проверка модели программы имеет серьезную проблему с взрывом пространства состояний (memory & disk usage). Но существует большое разнообразие методов для уменьшения проблем, для обработки больших артефактов, таких как частичное уменьшение порядка, абстракция, уменьшение симметрии и т. д.

Мы использовали несколько модельных шашек в обучении, системном проектировании и разработке систем. Наш набор инструментов включает в себя SPIN, UPPAL, Java Pathfinder, PVS и Bogor. У каждого есть свои сильные и слабые стороны. Все они находят проблемы с моделями, которые просто невозможно обнаружить человеческим существам. Их удобство использования варьируется, хотя большинство из них являются кнопочными автоматическими.

Когда использовать средство проверки моделей? Я бы сказал, что каждый раз, когда вы описываете модель, которая должна иметь (или не иметь) определенные свойства, и она больше, чем горстка понятий. Любой, кто думает, что может описать и понять что-то большее или более сложное, обманывает себя.

Я использовал SPIN, чтобы найти проблему параллелизма в программном обеспечении PLC. Он обнаружил неожиданное состояние гонки, которое было бы очень трудно обнаружить при проверке или тестировании.

Кстати, есть ли книга "SPIN for Dummies"? Мне пришлось выучить его из книги "The SPIN Model Checker" и различных онлайн-учебников.

Я провел некоторые исследования на эту тему во время моего пребывания в университете, расширяя штат исследования Assembly Model Checker .

Мы использовали виртуальную машину, чтобы обойти каждый возможный путь / состояние программы, используя A* и некоторые эвристические, в зависимости от вида ошибки (тупик, ошибки ввода-вывода,...)

Он был вдохновлен Java Pathfinder и работал с кодом C++. (Все, что может скомпилировать GCC)

Но, по нашему опыту, этот вид технологии не будет использоваться в бизнес-приложениях в ближайшее время из-за связанных с GUI проблем, работы, необходимой для создания начальной тестовой среды и огромных аппаратных требований. (Вам нужно много RAM и дискового пространства, из-за гигантского пространства состояний)