Что вы испытываете при проверке модели программного обеспечения?

Question

• Какие типы применений вы использовали model checking?
• Какой инструмент проверки модели вы использовали?
• Как бы вы суммировали свой опыт с техникой, в частности, оценивая ее эффективность в предоставлении более качественного программного обеспечения?

В ходе моих исследований, я имел возможность использовать Spin, и это вызвало мое любопытство относительно того, насколько фактическая проверка модели происходит и сколько ценности являются организации выхода из нее. В своем опыте работы я работал над бизнес-приложениями, где (естественно) нет необходимости применять формальную проверку к логике. Я бы очень хотел узнать о том, как SO проверяет опыт и мысли на эту тему. Будет ли модельная проверка когда-либо становиться более широко используемой развивающейся практикой, которую мы должны иметь в нашем инструментарии?

Answer 1

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

Хотя эти инструменты были забавны в использовании, я думаю, что они действительно сияют, когда вы объединяете их с чем-то, что динамически накладывает ограничения на вашу программу (так что немного легче проверить «полезные» вещи о вашей программе). В итоге мы получили Spring WebFlow framework, который использует XML для записи файла состояния, такого как файл, который указывает, какие веб-страницы могут перейти на другие, и используя SMV для выполнения проверки в указанных приложениях (shameless plug here).

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

Answer 2

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

Кстати, есть ли книга «SPIN for Dummies»? Я должен был изучить его из книги «Проверка SPIN Model Checker» и различных онлайн-руководств.

Answer 3

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

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

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

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

Answer 4

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

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

Answer 5

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

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

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

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

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

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