Проверка модели SPIN
 | В этой статье есть несколько проблем. Пожалуйста, помогите улучшить его или обсудите эти проблемы на странице обсуждения . ( Узнайте, как и когда удалять эти шаблонные сообщения )
|
| Разработчик(и) | Джерард Дж. Хольцманн |
|---|---|
| Первоначальный выпуск | 1989 |
| Стабильная версия | 6.5.2 / 6 декабря 2019 г |
| Репозиторий | |
| Написано в | С |
| Операционная система | Линукс Microsoft Windows Мак ОС Х |
| Доступно в | Английский |
| Тип | Проверка модели |
| Лицензия |
|
| Веб-сайт | http://spinroot.com/ |
SPIN проверки правильности параллельных моделей программного обеспечения — это общий инструмент для строгой и в основном автоматизированной . Оно было написано Джерардом Дж. Хольцманном и другими членами первоначальной группы Unix Исследовательского центра компьютерных наук Bell Labs , начиная с 1980 года. Программное обеспечение доступно бесплатно с 1991 года и продолжает развиваться, чтобы идти в ногу с новыми разработками в области компьютерных технологий. поле.
Инструмент [ править ]
Системы, подлежащие проверке, описываются в Promela (Process Meta Language), который поддерживает моделирование асинхронных распределенных алгоритмов как недетерминированных автоматов ( SPIN означает «Простой интерпретатор Promela»). Свойства, подлежащие проверке, выражаются в виде формул линейной временной логики (LTL) , которые инвертируются, а затем преобразуются в автоматы Бюхи как часть алгоритма проверки модели. Помимо проверки модели, SPIN также может работать как симулятор, прослеживая один из возможных путей выполнения в системе и предоставляя пользователю результирующую трассировку выполнения.
В отличие от многих средств проверки моделей, SPIN фактически не выполняет проверку модели самостоятельно, а вместо этого генерирует исходные коды C для средства проверки модели, специфичного для конкретной проблемы. Этот метод экономит память и повышает производительность, а также позволяет напрямую вставлять фрагменты кода C в модель. SPIN также предлагает большое количество опций для дальнейшего ускорения процесса проверки модели и экономии памяти, например:
- частичное сокращение заказа ;
- состояния сжатие ;
- хеширование битовых состояний (вместо хранения целых состояний в битовом поле запоминается только их хэш-код; это экономит много памяти, но аннулирует полноту );
- слабое обеспечение справедливости.
С 1995 года (приблизительно) ежегодно проводятся семинары по SPIN для пользователей SPIN, исследователей и тех, кто вообще интересуется проверкой моделей .
В 2001 году Ассоциация вычислительной техники наградила SPIN наградой за системное программное обеспечение. [1]
См. также [ править ]
Ссылки [ править ]
Дальнейшее чтение [ править ]
- Хольцманн, Г.Дж., Программа проверки моделей SPIN: учебник для начинающих и справочное руководство . Аддисон-Уэсли , 2004 г. ISBN 0-321-22862-6 .