Есть ли простой инструмент проверки модели. Я планирую реализовать средство проверки модели, которое будет анализировать код для некоторых предопределенных свойств.Простой инструмент проверки модели
ответ
Одним из важных инструментов является SPIN, с языком Promela. Если вы используете LaTeX, есть также TLA+.
Они не будут анализировать ваш код, но позволят вам выразить модель для ваших предположений и транзитных состояний и затем проанализировать недействительные состояния. Другими словами, они обнаружат проблемы в вашей модели, а не реализацию вашей модели.
Я видел демо Goanna, но я не знаю, доступен ли он вообще (коммерческий или иной); это имеет преимущество, фактически анализируя ваш исходный код.
Просто глядя на ваш вопрос и комментарии в своем вопросе снова, кажется, что вы действительно должны прочитать некоторые из литературы в первую очередь. Возможно, The Spin Model Checker, или Specifying Systems (можно загрузить с Leslie Lamport's website). Вам нужно пересмотреть свою проблему, чтобы вы не пытались решить проблему остановки.
CBMC - один простой инструмент, я знаю, что на самом деле работает на код. Проверка модели в целом - это тщательно изученная область, но, как уже отмечали люди, эта широта затрудняет предложение чего-то с предоставленной информацией. Существуют тысячи решателей SAT, формальные инструменты для проверки HDL/состояния машины и множество коммерческих анализаторов статических источников.
В любом случае, CBMC - хороший инструмент, но не верьте мне на слово; Эд Кларк, главный преподаватель за этой работой, получил премию Тьюринга в этом году ;-)
Средство проверки модели, которое поддерживает состояния. то есть я планирую реализовать Инструмент, который может сказать, прекращается ли приложение или нет. (Только статический анализ) – Vinay
Действительно? Это кажется немного сложным (http://en.wikipedia.org/wiki/Halting_problem) ;-) –
@MattJ сложно, но не невозможно. Если CBMC подтвердит правильность вашей программы и отсутствие ошибок/исключений во время выполнения, это также доказывает прекращение. Проблема с остановкой говорит только о том, что она не является тривиально разрешимой для всех программ, AFAIK. Для нескольких классов программ это тривиально разрешимо! +1 для упоминания CBMC, хотя это отличный инструмент. –
- 1. Инструмент для простой проверки кода IL
- 2. Простой автономный веб-сайт проверки инструмент
- 3. Простой инструмент для проверки реализации h2c
- 4. Простой инструмент обновления
- 5. Супер простой шаблонный инструмент
- 6. Простой инструмент управления проектами
- 7. Инструмент для проверки доставки?
- 8. Инструмент проверки кода Gerrit
- 9. Хороший инструмент проверки ссылок?
- 10. Инструмент проверки CSS
- 11. инструмент для проверки кода
- 12. Инструмент проверки HTML
- 13. Инструмент для проверки синтаксиса?
- 14. Инструмент для проверки масштабируемости
- 15. Инструмент модели JSON to NSObject
- 16. Простой графический инструмент для простой программы
- 17. Просмотр проверки модели и проверки модели домена
- 18. инструмент проверки орфографии и проверки javadoc
- 19. модели проверки в Backbone.js
- 20. SVG простой инструмент для рисования
- 21. Простой инструмент для создания MSI
- 22. Простой инструмент XML для mac
- 23. Пожалуйста, попробуйте простой инструмент xquery
- 24. Простой инструмент для изучения XQuery?
- 25. Хороший подход к созданию простой проверки модели в java
- 26. Инструмент или шаблон для проверки GWT
- 27. Любой простой инструмент для имитации загрузки сервера?
- 28. Инструмент проверки схемы показывает ошибки
- 29. Имеется ли инструмент проверки конфигурации?
- 30. Онлайн-инструмент для проверки Cran
Я думаю, вы должны попытаться объяснить немного ближе, что вы ищете ... –
Я думаю, вы должны пересмотреть свой вопрос, чтобы он был более ясным. Этот вопрос может относиться к десяткам различных сценариев проверки модели. –
Инструмент проверки модели, который поддерживает этапы. то есть я планирую реализовать Инструмент, который может сказать, прекращается ли приложение или нет. (Только статический анализ) – Vinay