Программа проверки моделей PRISM

PRISM — это программа проверки вероятностных моделей , формальный программный инструмент проверки для моделирования и анализа систем, демонстрирующих вероятностное поведение. ^{[ 1 ]} Одним из источников таких систем является использование рандомизации , например, в протоколах связи, таких как Bluetooth и FireWire , или в протоколах безопасности, таких как Crowds и Onion маршрутизация . Стохастическое поведение также возникает во многих других компьютерных системах, например, из-за сбоев оборудования, ненадежных датчиков и исполнительных механизмов или непредсказуемых задержек связи. PRISM использовалась для анализа широкого спектра приложений: от планирования роботов до анализа производительности компьютерных сетей и сетей биохимических реакций. ^{[ 2 ]}

PRISM может использоваться для анализа нескольких различных типов вероятностных моделей, включая цепи Маркова с дискретным временем , цепи Маркова с непрерывным временем , процессы принятия решений Маркова и вероятностные расширения формализма временных автоматов . Он также поддерживает вероятностные модели с частичной наблюдаемостью и понятия эпистемической неопределенности. Свойства, подлежащие проверке на основе этих моделей, выражаются в вероятностных расширениях темпоральной логики , таких как PCTL . Дополнительный инструмент PRISM PRISM-игры ^{[ 3 ]} обеспечивает анализ стохастических игр .

Разработкой PRISM руководит Оксфордский университет . Первоначально проект начался в Университете Бирмингема . Инструмент представляет собой программное обеспечение с открытым исходным кодом , выпущенное под лицензией GNU General Public License . PRISM был выбран для участия в программе Google Summer of Code в 2013 и 2014 годах. Инструмент и его создатели завоевали несколько наград: премию ETAPS Test-of-Time Tool Award 2024 и премию HVC 2016 .

Ссылки

^ Квятковска, М .; Норман, Г.; Паркер, Д. (2011). «ПРИЗМА 4.0: Верификация вероятностных систем реального времени». В Proc. 23-я Международная конференция по компьютерной проверке (CAV'11) , том 6806 конспектов лекций по информатике, страницы 585–591, Springer.
^ «Репозиторий тематических исследований PRISM» . Проверено 19 апреля 2024 г.
^ [[Квятковска, М.; Норман, Дж; Паркер, Д.; Сантос, Г. (2020). «PRISM-игры 3.0: стохастическая верификация игр с параллелизмом, равновесием и временем». В Proc. 32-я Международная конференция по компьютерной проверке (CAV'20) , том 12225 конспектов лекций по информатике, страницы 475–487, Springer.

Внешние ссылки

Эта формальным методам, статья, посвященная незавершена . Вы можете помочь Википедии, расширив ее .

[1] Квятковска, М .; Норман, Г.; Паркер, Д. (2011). «ПРИЗМА 4.0: Верификация вероятностных систем реального времени». В Proc. 23-я Международная конференция по компьютерной проверке (CAV'11) , том 6806 конспектов лекций по информатике, страницы 585–591, Springer.

[2] «Репозиторий тематических исследований PRISM» . Проверено 19 апреля 2024 г.

[3] [[Квятковска, М.; Норман, Дж; Паркер, Д.; Сантос, Г. (2020). «PRISM-игры 3.0: стохастическая верификация игр с параллелизмом, равновесием и временем». В Proc. 32-я Международная конференция по компьютерной проверке (CAV'20) , том 12225 конспектов лекций по информатике, страницы 475–487, Springer.

[ 1 ]

[ 2 ]

[ 3 ]