#model-checking #spin
#проверка модели #вращение
Вопрос:
Кто-нибудь сталкивался с проверкой модели с помощью этого инструмента SPIN, более того, с какой-либо информацией о проверке модели (параллельные программы)
Ответ №1:
Да, SPIN — очень хороший средство проверки модели, но мне интересно, чего вы хотите? Вы просто хотите услышать, что да, я слышал и играл с SPIN, или вам нужны предложения о том, как моделировать исходный код проверки?
Например, если вы программист на C, залезьте в ESBMC, напишите небольшую программу и запустите в ней ESBMC.
Это должно помочь вам начать понимать, что можно сделать и как это сделать. Кстати, для начала Проверка модели — это не статический анализ. На самом деле это намного мощнее. Это антистатический анализ. Проверка модели фактически «в (очень узком) смысле» имитирует вашу программу и находит ситуации (комбинации аргументов, исключительные ситуации, пограничные случаи), где это действительно приведет к сбою.
Комментарии:
1. А? Это точно статический анализ: он основывается на исходном коде. Вы можете возразить, что это отличается от других статических анализаторов, но я не вижу, какой в этом смысл; они все разные.
2. Извините, это не так. Код анализируется динамически, поэтому он не является статичным. Средства проверки моделей не выполняют код «как таковой», но генерируют модели, которые моделируются. Следовательно, это не статический анализ. lint — это статический анализатор. ВРАЩЕНИЕ — нет.
3. Я думаю, что ваши определения запутаны. Динамический анализ означает сбор информации по мере выполнения программы . С помощью SPIN вы извлекаете абстрактную модель программы (обычно используя статический анализ!), а затем SPIN перечисляет пространство состояний. Моделирование пространства состояний не имеет ничего общего с выполнением программы. На данный момент нет «программы» для выполнения.
4. SPIN НЕ является статическим анализатором. Для тех, кто все еще сомневается, обратитесь к: Обзор статических анализаторов C , Статический анализ программ , Динамический анализ программ . Также обратите внимание, что извлечение модели Promela из исходных текстов C далеко не тривиальная или широко автоматизированная процедура и, безусловно, само по себе полностью отличается от статического анализа. Кроме того, имитация пространства состояний ЯВЛЯЕТСЯ выполнением программы. Из-за взрыва пространства состояний обычно мы используем частичное моделирование.