2 работы из ссылок Parallel Breadth-First Search LTL Model-Checking

Просмотреть остальные работы.

Разобраться, как работают state compression и partial order reduction (особенно последнее).

Изучить работу SPIN, генерируемый код, возможности.

Перечитать описание PROMELA.

ТЕМА: Параллельное построение пространства состояний конечной системы.

Диплом

Актуальность: На данный момент основным программным средством для подобной проверки является SPIN (использующий язык описания PROMELA), существенным недостатком которого является невозможность использовать вычислительные ресурсы, в первую очередь память, более чем одной машины. Притом, задача построения пространства состояний модели имеет экспоненциально растующие требования памяти и вычислительной мощности, что приводит к крайне длительной проверки моделей даже среднего размера. Имеется лишь один аналог, способный осуществлять параллельное построение множества состояний – DiVinE, разработанный в университете Брно, однако он пока является экспериментальным продуктом.

Аналитический раздел

Анализ существующих средств параллельных вычислений (копипаста, хм, из прошлого диплома).

Анализ распределения состояний по узлам кластера: подбор функции распределения, определение критериев оптимальности распределения

[ Анализ подходов к проверке LTL-формул при поиске в глубину и в ширину. ]

Конструкторский раздел

Проектирование схемы распределения вычислений между узлами.

Проектирование генерации кода перехода между состояниями.

[ Проектирование алгоритма поиска допускающих циклов. ]

Технологический раздел

Реализация, тестирование.

Исследовательнский раздел

Проведение экспериментов: сравнение со SPIN, сравнение с аналогичными исследованиями в университете Брно.

Заключение: прирост в производительности в сравнении со SPIN на моделях среднего размера (требующих большего объема памяти, чем доступно на отдельной машине).

Бланк

Проанализировать применимость распараллеливания к данной задаче, изучить существующие аналоги.

Проанализировать известные оптимизации, применяемые при построении пространства состояний, оценить их применимость в параллельном варианте

Определить критерии оптимальности распределения состояний по узлам, выбрать оптимальное распределение

Спроектировать и реализовать алгоритм параллельной генерации состояний.

Спроектировать и реализовать транслятор описания системы на некотором языке в функцию перехода между состояниями.

Провести тестирование и эксперименты, проанализировать экспериментальные данные.

Семинар

Актуальность: при решении задачи построения пространства состояний конечной системы, например, при верификации протоколов, происходит “комбинаторный взрыв” количества состояний для систем уже среднего размера, что делает традиционный способ решения крайне медленным. Размер, необходимый для хранения пространства состояний, может легко превысить объем доступной памяти, поэтому традиционные средства, например, SPIN, верифицирующий протоколы, описанные на языке PROMELA, являются малоэффективными для таких систем. Задача проектирования и реализации средства, выполняющего параллельное построение пространства состояний, является, следовательно, актуальной.

Задачи:

Анализ применимости распараллеливания к задаче построение пространства состояний

Определение критериев оптимальности и выбор оптимального распределения состояний по узлам вычисления.

Определение применимости различных оптимизаций, используемых при традиционном построении пространства состояний.

Проектирование и реализация алгоритма параллельного построения.

Проектирование и реализация транслятора описания системы в функцию перехода между состояниями [я вот не уверен, следует ли об этом. хотя это вообще-то самое большое по фактическому объему %)]

Тестирование реализованного алгоритма и проведение экспериментов.

Интерпретация результатов.

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