научное издание МГТУ им. Н.Э. Баумана
НАУКА и ОБРАЗОВАНИЕ
Издатель ФГБОУ ВПО "МГТУ им. Н.Э. Баумана". Эл № ФС 77 - 48211. ISSN 1994-0408
# 03, март 2012
Korot-Kri.pdf
(348.02Кб)
УДК 004.021
МГТУ им. Н.Э. Баумана
При проверке конечных дискретных моделей для обхода ограничений, накладываемых объемом доступной памяти, может использоваться параллельная генерация и распределенное хранение пространства состояний. Эффективность такого подхода зависит от выбора функции распределения состояний между вычислительными узлами. Рассмотрен выбор этой функции, позволяющий уменьшить время проверки модели за счет уменьшения числа удаленных вызовов между узлами. Приведены результаты экспериментов, полученные при помощи прототипа средства для проверки моделей.
Список литературы
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.
Публикации с ключевыми словами: параллельные вычисления, проверка моделей, генерация состояний
Публикации со словами: параллельные вычисления, проверка моделей, генерация состояний
Смотри также:
Тематические рубрики:
| Авторы |
| Пресс-релизы |
| Библиотека |
| Конференции |
| Выставки |
| О проекте |
| Телефон: +7 (915) 336-07-65 (строго: среда; пятница c 11-00 до 17-00) |
|
 |
|||
| © 2003-2024 «Наука и образование» Перепечатка материалов журнала без согласования с редакцией запрещена Тел.: +7 (915) 336-07-65 (строго: среда; пятница c 11-00 до 17-00) | |||||
