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

научное издание МГТУ им. Н.Э. Баумана

НАУКА и ОБРАЗОВАНИЕ

Издатель ФГБОУ ВПО "МГТУ им. Н.Э. Баумана". Эл № ФС 77 - 48211.  ISSN 1994-0408

77-30569/342044 Выбор функции распределения состояний при параллельной проверке модели

# 03, март 2012
Файл статьи: Korot-Kri.pdf (348.02Кб)
авторы: Коротков И. А., Крищенко В. А.

УДК 004.021

МГТУ им. Н.Э. Баумана

korotkov2@mail.ru

kva@bmstu.ru

 

При проверке конечных дискретных моделей для обхода ограничений, накладываемых объемом доступной памяти, может использоваться параллельная генерация и распределенное хранение пространства состояний. Эффективность такого подхода зависит от выбора функции распределения состояний между вычислительными узлами. Рассмотрен выбор этой функции, позволяющий уменьшить время проверки модели за счет уменьшения числа удаленных вызовов между узлами. Приведены результаты экспериментов, полученные при помощи прототипа средства для проверки моделей.

 

Список литературы

1. Э.М. Кларк, О. Грамберг, Д. Пелед. Верификация моделей программ. Model Checking. Москва: МЦ-НМО, 2002. 416 c.

2. Holzmann, G.J. An Analysis of Bitstate Hashing // Formal Methods in System Design. 1998. Vol. 13, N. 3. Pp. 287–305.

3. Holzmann, G.J. The model checker SPIN // IEEE Transactions on Software Engineering. 1997. Vol. 23. Pp. 279–295.

Поделиться:
 
ПОИСК
 
elibrary crossref ulrichsweb neicon rusycon
 
ЮБИЛЕИ
ФОТОРЕПОРТАЖИ
 
СОБЫТИЯ
 
НОВОСТНАЯ ЛЕНТА



Авторы
Пресс-релизы
Библиотека
Конференции
Выставки
О проекте
Rambler's Top100
Телефон: +7 (915) 336-07-65 (строго: среда; пятница c 11-00 до 17-00)
  RSS
© 2003-2017 «Наука и образование»
Перепечатка материалов журнала без согласования с редакцией запрещена
 Тел.: +7 (915) 336-07-65 (строго: среда; пятница c 11-00 до 17-00)