Проверка модели SPIN

Инструмент для проверки правильности моделей программного обеспечения

SPIN

Разработчик (ы))	Gerard J. Holzmann
Первоначальный выпуск	1989 (1989)
Стабильный выпуск	6.5.2 / 6 декабря 2019 г.; 10 месяцев назад (06.12.2019)
Репозиторий	github.com / nimble-code / Spin
Написано в	C
Операционной системе	Linux. Microsoft Windows. Mac OS X
Доступно на	английском языке
Тип	Проверка модели
Лицензия	Лицензия BSD с тремя пунктами (начиная с версии 6.4.5) Общественная лицензия на программное обеспечение SPIN (предыдущие версии)
Веб-сайт	http://spinroot.com/

SPIN - это общий инструмент для проверки правильности параллельного программного обеспечения моделирование строго и в основном автоматизировано. Он был написан Джерардом Дж. Хольцманном и другими сотрудниками первоначальной группы Unix Исследовательского центра вычислительных наук в Bell Labs, начиная с 1980 года. Программное обеспечение было свободно доступно с 1991 года. и продолжает развиваться, чтобы идти в ногу с новыми разработками в этой области.

• 1 Инструмент
• 2 См. Также
• 3 Ссылки
• 4 Дополнительная литература
• 5 Внешние ссылки

Системы, подлежащие проверке, описаны в Promela (Process Meta Language), который поддерживает моделирование асинхронных распределенных алгоритмов как недетерминированных автоматов (SPIN означает «Простой переводчик Promela»). Проверяемые свойства выражаются в виде формул линейной временной логики (LTL), которые инвертируются и затем преобразуются в автоматы Бюхи в рамках алгоритма проверки модели. Помимо проверки модели, SPIN также может работать как симулятор, следуя одному из возможных путей выполнения в системе и представляя пользователю полученную трассировку выполнения.

В отличие от многих средств проверки моделей, SPIN на самом деле не выполняет проверку модели, а вместо этого создает исходные коды C для средства проверки конкретной проблемы. Этот метод экономит память и повышает производительность, а также позволяет напрямую вставлять фрагменты кода C в модель. SPIN также предлагает большое количество опций для дальнейшего ускорения процесса проверки модели и экономии памяти, таких как:

• частичное уменьшение порядка ;
• состояние сжатие ;
• хеширование состояния бит (вместо сохранения Для всех штатов в битовом поле запоминается только их хэш-код; это экономит много памяти, но отменяет полноту );
• слабое обеспечение справедливости.

С 1995 года (приблизительно) ежегодные семинары SPIN проводились для пользователей SPIN, исследователи и те, кто обычно интересуется проверкой моделей.

В 2001 году Association for Computing Machinery наградила SPIN своей наградой за системное программное обеспечение.

• NuSMV
• Uppaal Model Checker

1. ^Награда за программную систему: ACM CITES TOOL ДЛЯ ОБНАРУЖЕНИЯ «ОШИБОК» ПРОГРАММНОГО ОБЕСПЕЧЕНИЯ ДЛЯ ПРЕСТИЖНОЙ НАГРАДЫ. Исследователь Bell Labs разработал «SPIN», чтобы сделать компьютеры более надежными // Пресс-релиз ACM

• Holzmann, GJ, The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley, 2004. ISBN 0-321-22862-6.

• Веб-сайт SPIN