SPIN-проверка модели
 | В этой статье есть несколько проблем. Помогите улучшить ее или обсудите эти проблемы на странице обсуждения . ( Узнайте, как и когда удалять эти сообщения )
|
| Разработчик(и) | Джерард Дж. Хольцманн |
|---|---|
| Первоначальный выпуск | 1989 ( 1989 ) |
| Стабильный релиз | 6.5.2 / 6 декабря 2019 г. ( 2019-12-06 ) |
| Репозиторий |
|
| Написано в | С |
| Операционная система | LinuxМайкрософтВиндовсMac OS X |
| Доступно в | Английский |
| Тип | Проверка модели |
| Лицензия |
|
| Веб-сайт | http://spinroot.com/ |
SPIN — это общий инструмент для проверки корректности параллельных программных моделей в строгом и в основном автоматизированном режиме. Он был написан Джерардом Дж. Хольцманном и другими в оригинальной группе Unix Исследовательского центра вычислительных наук в Bell Labs , начиная с 1980 года. Программное обеспечение доступно бесплатно с 1991 года и продолжает развиваться, чтобы идти в ногу с новыми разработками в этой области.
Инструмент
Системы, подлежащие проверке, описаны в Promela (Process Meta Language), который поддерживает моделирование асинхронных распределенных алгоритмов как недетерминированных автоматов ( SPIN означает «Simple Promela Interpreter»). Свойства, подлежащие проверке, выражаются в виде формул линейной временной логики (LTL) , которые отрицаются и затем преобразуются в автоматы Бюхи в рамках алгоритма проверки модели. В дополнение к проверке модели SPIN также может работать как симулятор, следуя одному возможному пути выполнения через систему и представляя пользователю полученную трассировку выполнения.
В отличие от многих проверяющих моделей, SPIN фактически не выполняет проверку модели сам, а вместо этого генерирует исходники C для проверяющего модели, специфичного для проблемы. Этот метод экономит память и повышает производительность, а также позволяет напрямую вставлять фрагменты кода C в модель. SPIN также предлагает большое количество опций для дальнейшего ускорения процесса проверки модели и экономии памяти, например:
- частичная редукция порядка ;
- сжатие состояния ;
- хеширование битовых состояний (вместо хранения целых состояний в битовом поле запоминается только их хеш-код; это экономит много памяти, но лишает полноты );
- слабое обеспечение справедливости.
Начиная с 1995 года (примерно) ежегодно проводятся семинары SPIN для пользователей SPIN, исследователей и всех, кто интересуется проверкой моделей .
В 2001 году Ассоциация вычислительной техники наградила SPIN своей премией за системное программное обеспечение. [1]
Смотрите также
Ссылки
- ^ Премия за лучшую программную систему: ACM НОСИЛА ПРЕСТИЖНУЮ НАГРАДУ ИНСТРУМЕНТУ ДЛЯ ОБНАРУЖЕНИЯ «ОШИБОК» ПРОГРАММНОГО ОБЕСПЕЧЕНИЯ. Исследователь из Bell Labs разработал «SPIN», чтобы сделать компьютеры более надежными // Пресс-релиз ACM
Дальнейшее чтение
- Хольцманн, Г. Дж., SPIN Model Checker: Primer and Reference Manual . Addison-Wesley , 2004. ISBN 0-321-22862-6 .
Внешние ссылки
- веб-сайт СПИН
