Инструмент проверки простых моделей
Есть ли простой инструмент проверки моделей. Я планирую реализовать инструмент проверки моделей, который будет анализировать код некоторых предопределенных свойств.
Думаю, вам стоит пересмотреть свой вопрос, чтобы он был более ясным. Этот вопрос может относиться к десятку различных сценариев проверки модели.
Инструмент проверки модели, который поддерживает состояние. то есть я планирую реализовать инструмент, который может сказать, завершается ли приложение или нет. (Только статический анализ)
Ой-ой ... это известно как проблема остановки (en.wikipedia.org/wiki/Halting_problem), и было показано, что ее невозможно решить :-)
Проблема остановки неразрешима. Это не означает, что анализ не может быть выполнен: en.wikipedia.org/wiki/Termination_analysis
Ответы 2
CBMC - один простой инструмент, о котором я знаю, который на самом деле работает с кодом. Проверка моделей в целом - это хорошо изученная область, но, как люди уже отметили, такая широта затрудняет предложение чего-либо с предоставленной информацией. Существуют тысячи решателей SAT, формальные инструменты для проверки HDL / конечного автомата и множество коммерческих статических анализаторов источников.
В любом случае CBMC - хороший инструмент, но не верьте мне на слово; Эд Кларк, главный преподаватель этой работы, получил в этом году премию Тьюринга ;-)
Инструмент проверки модели, который поддерживает состояния. то есть я планирую реализовать инструмент, который может сказать, завершается ли приложение или нет. (Только статический анализ)
Действительно? Это кажется немного сложным (en.wikipedia.org/wiki/Halting_problem) ;-)
@MattJ сложно, но возможно. если CBMC доказывает правильность вашей программы и отсутствие ошибок / исключений во время выполнения, это также доказывает завершение работы. Проблема остановки говорит только о том, что она не решима тривиально для всех программ, AFAIK. Для нескольких классов программ это тривиально разрешимо! +1 за упоминание CBMC, это отличный инструмент.
Одним из важных инструментов является ВРАЩЕНИЕ с языком Promela. Если вы используете LaTeX, есть еще TLA +.
Они не будут анализировать ваш код, но позволят вам выразить модель для ваших предположений и переходов состояний, а затем проанализировать недопустимые состояния. Другими словами, они обнаружат проблемы в вашей модели, а не в ее реализации.
Я видел демонстрацию Goanna, но не знаю, доступна ли она вообще (коммерческая или нет); это имеет то преимущество, что фактически анализирует ваш исходный код.
Просто глядя на свой вопрос и снова на комментарии к нему, кажется, что вам действительно стоит сначала прочитать некоторую литературу. Возможно, Проверка модели вращения или Определение систем (загружается с Сайт Лесли Лэмпорта). Вам нужно переосмыслить свою проблему, чтобы не пытаться решить проблему остановки.
Думаю, тебе стоит попытаться немного подробнее объяснить, что ты ищешь ...