Каков ваш опыт проверки моделей программного обеспечения?[закрыто]

Question

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

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

Answer 1

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

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

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

Answer 2

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

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

Answer 3

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

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

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

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

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

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

Answer 4

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

Кстати, есть ли книга "СПИН для чайников"?Мне пришлось изучить это из книги «Проверка моделей SPIN» и различных онлайн-уроков.

Answer 5

Во время учебы в университете я провел некоторое исследование по этому вопросу, расширив Средство проверки модели сборки состояния.

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

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

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