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

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

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

5 ОТВЕТОВ
РЕШЕНИЕ

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

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

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

3
24.08.2008 18:17:20

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

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

0
25.11.2008 22:46:46
Я хотел бы предложить Принципы проверки моделей SPIN как наиболее близкие к книге «SPIN для чайников».
Ioannis Filippidis 16.07.2013 09:10:21

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

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

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

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

0
26.01.2009 12:51:37

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

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

2
24.10.2009 10:38:30

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

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

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

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

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

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

2
10.06.2012 10:57:29