WikiDer > Программа проверки моделей PRISM - Википедия
ПРИЗМА вероятностный модель проверки, а формальная проверка программный инструмент для моделирования и анализа систем, демонстрирующих вероятностное поведение.[1][2] Одним из источников таких систем является использование рандомизация, например, в таких протоколах связи, как Bluetooth и FireWire, или в протоколах безопасности, таких как Толпы и Луковая маршрутизация. Стохастическое поведение также возникает во многих других компьютерных системах, например, из-за отказов оборудования или непредсказуемых задержек связи. Еще один класс систем, поддающихся такому анализу: биохимический сети реакции.
PRISM может использоваться для анализа нескольких различных типов вероятностных моделей, в том числе цепи Маркова с дискретным временем, цепи Маркова с непрерывным временем, Марковские процессы принятия решений и вероятностные расширения синхронизированные автоматы формализм. Свойства, которые необходимо проверить на соответствие этим моделям, выражаются в вероятностных расширениях темпоральная логика.
Разработка PRISM в основном ведется на Бирмингемский университет и Оксфордский университет. Инструмент программное обеспечение с открытым исходным кодом, выпущенный под Стандартная общественная лицензия GNU. PRISM была выбрана для Google Summer of Code программа в 2013 и 2014 годах.
Рекомендации
- ^ Квятковская, М.; Norman, G .; Паркер, Д. (2011). «ПРИЗМА 4.0: Верификация вероятностных систем реального времени». В Proc. 23-я Международная конференция по компьютерной верификации (CAV’11), том 6806 конспектов лекций по информатике, страницы 585-591, Springer.
- ^ Квятковская, М .; Norman, G .; Паркер, Д. «Вероятностная модель проверки на практике: примеры использования PRISM». Обзор оценки эффективности ACM SIGMETRICS, 32 (4), страницы 16–21.
внешняя ссылка
 | Этот формальные методы-связанная статья является заглушка. Вы можете помочь Википедии расширяя это. |