Есть ли у кого-нибудь контакт с проверкой моделей с помощью этого инструмента SPIN, а тем более любой информации проверка модели (параллельные программы)
Spin — формальная проверка
Ответы (1)
Да, SPIN — очень хорошая программа для проверки моделей, но мне интересно, что вы хотите? Вы просто хотите услышать, что да, я слышал и играл со SPIN, или вам нужны предложения о том, как моделировать исходный код?
Например, если вы программист на C, попробуйте ESBMC. , напишите небольшую программу и запустите на ней ESBMC.
Это должно помочь вам начать понимать, что можно сделать и как это сделать. Кстати, для начала проверка модели — это не статический анализ. На самом деле он намного мощнее. Это антистатический анализ. Проверка модели на самом деле «в (очень узком) смысле» моделирует вашу программу и находит ситуации (комбинации аргументов, исключительные ситуации, пограничные случаи), в которых она на самом деле потерпит неудачу.
person
Paulo Matos
schedule
20.07.2011
А? Это точно статический анализ: он исходит из исходного кода. Вы можете возразить, что он отличается от других статических анализаторов, но я не вижу в этом смысла; они все разные.
- person Ira Baxter; 20.07.2011
Извините, это не так. Код анализируется динамически, поэтому он не статичен. Средства проверки моделей не выполняют код «как таковой», а генерируют симулированные модели. Следовательно, это не статический анализ. lint — статический анализатор. СПИН нет.
- person Paulo Matos; 28.07.2011
Я думаю, что ваши определения запутаны. Динамический анализ означает получение информации во время работы программы. С помощью SPIN вы извлекаете абстрактную модель программы (обычно с помощью статического анализа!), а затем SPIN перечисляет пространство состояний. Моделирование пространства состояний не имеет ничего общего с выполнением программы. На данный момент нет программы для выполнения.
- person Ira Baxter; 28.07.2011
SPIN НЕ является статическим анализатором. Для тех, кто все еще сомневается, обратитесь к: Обзор статических анализаторов C, Статический анализ программы, Динамический анализ программы. Кроме того, обратите внимание, что извлечение модели Promela из исходных кодов C — далеко не тривиальная или широко автоматизированная процедура и, безусловно, сама по себе полностью отличается от статического анализа. А также моделирование выполнения программы ИС в пространстве состояний. Из-за взрыва пространства состояний обычно мы используем частичное моделирование.
- person Ioannis Filippidis; 26.07.2013
