РУсскоязычный Архив Электронных СТатей периодических изданий
Инженерный журнал: наука и инновации/2012/№ 11/
В наличии за
50 руб.
Купить
Облако ключевых слов*
* - вычисляется автоматически
Недавно смотрели:

ПОДХОД К ПОИСКУ ВЗАИМНЫХ БЛОКИРОВОК В МНОГОПОТОЧНОМ ПРОГРАММНОМ ОБЕСПЕЧЕНИИ С ПОМОЩЬЮ ВЕРИФИКАТОРА SPIN

Рассмотрена задача поиска потенциальных взаимных блокировок в многопоточном программном обеспечении. Предложен подход к выявлению потенциальных взаимных блокировок в многопоточных программных комплексах на основе метода Model Checking. Описано, каким образом основные примитивы синхронизации могут быть представлены на входном языке верификатора SPIN. Приведен пример моделирования и выявления взаимной блокировки в многопоточной программе.

Авторы
Тэги
Тематические рубрики
Предметные рубрики
В этом же номере:
Резюме по документу**
П а р ф и л о в ПОДХОД К ПОИСКУ ВЗАИМНЫХ БЛОКИРОВОК В МНОГОПОТОЧНОМ ПРОГРАММНОМ ОБЕСПЕЧЕНИИ С ПОМОЩЬЮ ВЕРИФИКАТОРА SPIN Рассмотрена задача поиска потенциальных взаимных блокировок в многопоточном программном обеспечении. <...> Предложен подход к выявлению потенциальных взаимных блокировок в многопоточных программных комплексах на основе метода Model Checking. <...> Описано, каким образом основные примитивы синхронизации могут быть представлены на входном языке верификатора SPIN. <...> Приведен пример моделирования и выявления взаимной блокировки в многопоточной программе. <...> Одним из признаков нестабильной работы многопоточной программы является возникновение взаимной блокировки потоков в процессе их выполнения. <...> Взаимные блокировки происходят в результате некорректного использования средств синхронизации потоков, когда имеется группа потоков, каждый из которых пытается получить эксклюзивный доступ к некоторым ресурсам и претендует на ресурсы, принадлежащие другому потоку. <...> Для решения проблемы возникновения взаимных блокировок на этапе детализированного проектирования целесообразно использовать технологии верификации, основанные на методе Model Checking [3, 4]. <...> Верификация программных систем с помощью метода Model Checking состоит из 86 ISSN 0236-3933. <...> Рассмотрим подход к выявлению потенциальных взаимных блокировок в многопоточных программах, основанный на методе Model Checking. <...> Он заключается в построении схемы использования потоками средств синхронизации, спецификации этой схемы на языке Promela и ее анализа с помощью верификатора SPIN [5]. <...> Он способен выявлять в моделях программ взаимную блокировку, недостижимые участки кода, а также определять выполнимость LTL-спецификаций. <...> Для построения модели по исходной программе или алгоритму пользователь (обычно вручную) строит представление этой программы на С-подобном входном языке пакета SPIN, носящем название Promela (Protocol Meta Language). <...> Это представление (программу на языке Promela) можно считать <...>
** - вычисляется автоматически, возможны погрешности

Похожие документы: