Машиностроение
Приборостроение
Методическая периодика: проблемы и решения
Организация производства (промышленность)

Ключевые слова
Аннотации
Архив рубрик

регистрация
забыли пароль?

Другие журналы

электронный научно-технический журнал

ИНЖЕНЕРНЫЙ ВЕСТНИК

Издатель: Общероссийская общественная организация "Академия инженерных наук им. А.М. Прохорова".

Поиск взаимных блокировок в многопоточных системах: проверка целостности сильно связных компонент

Инженерный вестник # 09, сентябрь 2014
УДК: 519.68/69

Файл статьи:

Andreev_A.pdf (659.50Кб)

авторы: Андреев А. М., Козлов И. А.

Одним из путей решения этой проблемы является верификация моделей по методу Model Checking. Анализу подвергается модель многопоточной системы, представляющая собой ориентированный граф, рёбра которого отражают зависимости между потоками. В основе верифицирующего алгоритма для обнаружения взаимных блокировок лежит поиск сильно связных компонент (ССК) в этом графе. В статье изложен метод проверки целостности сильно связных компонент в рамках алгоритма поиска взаимных блокировок в многопоточных системах. Приведено краткое описание модели многопоточной системы и верифицирующего алгоритма. Описаны основные принципы подхода и приёмы, используемые для уменьшения вычислительной сложности.

Список литературы
1. Э. Кларк, О. Грамберг, Д. Пелед. Верификация моделей программ: Model Checking. – М.: МНЦМО, 2002. –416 с.
2. Ю. Карпов. Model Checking верификация параллельных и распределенных программных систем. – СПб.: БХВ-Петербург, 2010. –560 с.
3. Кузьмин Е. В., Соколов В. А. О дисциплине специализации «Верификация программ» // Доклады II научно-методической конференции «Преподавание математики в компьютерных науках» Ярославль: ЯрГУ. 2007. С. 91-101
4. Вельдер С.Э, Лукин М.А., Шалыто А.А., Яминов Б.Р. Верификация автоматных программ. СПбГУ ИТМО, 2011. – 240 с.
5. Андреев А.М., Козлов И.А. Подход к верификации моделей систем реального времени с помощью метода Model Checking. – Вестник МГТУ им. Н.Э.Баумана. Серия «Приборостроение». 2012. Специальный выпуск «Моделирование и идентификация компьютерных систем и сетей» – 47 с.
6. Свирин Ил.С., Силин П.А., Сюзев В.В. Математическая модель многопоточной программы и правила безопасности многопоточного программирования. – Вестник МГТУ им. Н.Э.Баумана. Серия «Приборостроение». 2012. Специальный выпуск «Моделирование и идентификация компьютерных систем и сетей» – 95 с.
7. Свирин Ил.С., Силин П.А., Сюзев В.В, Зарецкая Е.А. Математическая модель взаимных блокировок. Корректное использование исключающих семафоров. – Вестник МГТУ им. Н.Э.Баумана. Серия «Приборостроение». 2012. Специальный выпуск «Моделирование и идентификация компьютерных систем и сетей» – 112 с.
8. Р. Седжвик. Фундаментальные алгоритмы на С++. Алгоритмы на графах: Пер. с англ. – СПб: ООО «ДиаСофтЮП», 2002. – 688 с.