Libdmc - Libdmc
| Разработчики) | Александр Хамес |
|---|---|
| Операционная система | Posix Системы |
| Тип | Проверка модели |
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.
- ^ Хамес, Александр; Кордон, Фабрис; Тьерри-Миг, Янн; Легон-Обри, Фабрис (2007). «dmcG: Распределенная проверка символьных моделей на основе GreatSPN». Конспект лекций по информатике. 4546: 495–504. Дои:10.1007/978-3-540-73094-1_29. ISBN 978-3-540-73093-4.
- ^ Accueil LIP6
  | Эта статья по биоинформатике заглушка. Вы можете помочь Википедии расширяя это. |
 | Этот Unix -связанная статья является заглушка. Вы можете помочь Википедии расширяя это. |