Простой инструмент проверки модели

Question

Есть ли простой инструмент проверки модели. Я планирую реализовать средство проверки модели, которое будет анализировать код для некоторых предопределенных свойств.

Answer 1

Одним из важных инструментов является SPIN, с языком Promela. Если вы используете LaTeX, есть также TLA+.

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

Я видел демо Goanna, но я не знаю, доступен ли он вообще (коммерческий или иной); это имеет преимущество, фактически анализируя ваш исходный код.

Просто глядя на ваш вопрос и комментарии в своем вопросе снова, кажется, что вы действительно должны прочитать некоторые из литературы в первую очередь. Возможно, The Spin Model Checker, или Specifying Systems (можно загрузить с Leslie Lamport's website). Вам нужно пересмотреть свою проблему, чтобы вы не пытались решить проблему остановки.

Answer 2

CBMC - один простой инструмент, я знаю, что на самом деле работает на код. Проверка модели в целом - это тщательно изученная область, но, как уже отмечали люди, эта широта затрудняет предложение чего-то с предоставленной информацией. Существуют тысячи решателей SAT, формальные инструменты для проверки HDL/состояния машины и множество коммерческих анализаторов статических источников.

В любом случае, CBMC - хороший инструмент, но не верьте мне на слово; Эд Кларк, главный преподаватель за этой работой, получил премию Тьюринга в этом году ;-)