Libdmc
Разработчик(и) | Александр Хамез |
---|---|
Операционная система | Позикс -системы |
Тип | Проверка модели |
Libdmc [1] [2] это библиотека, разработанная на LIP6 [3] лаборатория. Его цель — облегчить распространение существующих средств проверки моделей . Он также был разработан для предоставления наиболее универсальных интерфейсов без ущерба для производительности благодаря языку C++ .
Проверка модели предлагает способ автоматически доказать правильность поведения смоделированной системы путем проверки свойств. Однако он страдает от так называемой проблемы «пространственного взрыва состояний», вызванной интенсивным использованием памяти. Для преодоления этой проблемы было предложено множество решений (например, символические представления с диаграммами решений — например, BDD ), но эти методы могут быстро привести к неприемлемым затратам времени.
Проверка распределенной модели — это способ снизить потребление памяти и времени за счет использования агрегированных ресурсов выделенного кластера. Однако переписать всю программу проверки модели — сложная задача, поэтому подход libdmc состоит в том, чтобы предоставить основу для создания средства проверки модели.
Ссылки
[ редактировать ]- ^ Хамез, Александр; Кордон, Фабрис; Тьерри-Миг, Ян (2007). «IibDMC: библиотека для эффективной проверки распределенных моделей». 2007 Международный симпозиум IEEE по параллельной и распределенной обработке . стр. 1–8. дои : 10.1109/IPDPS.2007.370647 . ISBN 978-1-4244-0909-9 . S2CID 12586847 .
- ^ Хамез, Александр; Кордон, Фабрис; Тьерри-Миг, Янн; Легон-Обри, Фабрис (2007). «DMCG: средство проверки распределенных символических моделей на основе GreatSPN». Сети Петри и другие модели параллелизма – ICATPN 2007 . Конспекты лекций по информатике. Том. 4546. стр. 495–504. дои : 10.1007/978-3-540-73094-1_29 . ISBN 978-3-540-73093-4 .
- ^ Главная LIP6