ПОДХОД К ПОИСКУ ВЗАИМНЫХ БЛОКИРОВОК В МНОГОПОТОЧНОМ ПРОГРАММНОМ ОБЕСПЕЧЕНИИ С ПОМОЩЬЮ ВЕРИФИКАТОРА 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) можно считать <...>

• Похожие документы из РУАЭСТ
• |
• Похожие документы из Руконт