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

Question

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

Answer 1

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

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

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

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

Answer 2

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

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