Kontrola modelu PRISM - PRISM model checker - Wikipedia

HRANOL je pravděpodobnostní kontrola modelu, a formální ověření softwarový nástroj pro modelování a analýzu systémů, které vykazují pravděpodobnostní chování.[1][2] Jedním ze zdrojů těchto systémů je použití randomizace, například v komunikačních protokolech jako Bluetooth a FireWire, nebo v bezpečnostních protokolech, jako je Davy a Směrování cibule. Stochastické chování se objevuje také v mnoha jiných počítačových systémech, například kvůli poruchám zařízení nebo nepředvídatelným zpožděním komunikace. Ještě další třída systémů přístupná tomuto druhu analýzy jsou biochemické reakční sítě.

PRISM lze použít k analýze několika různých typů pravděpodobnostních modelů, včetně diskrétní Markovovy řetězce, Markovovy řetězce nepřetržitého času, Markovovy rozhodovací procesy a pravděpodobnostní rozšíření časované automaty formalismus. Vlastnosti, které mají být ověřeny proti těmto modelům, jsou vyjádřeny v pravděpodobnostních rozšířeních časová logika.

Vývoj PRISMU se primárně provádí na University of Birmingham a University of Oxford. Nástroj je open-source software, vydané pod GNU General Public License. PRISM byl vybrán pro Google Summer of Code programu v letech 2013 a 2014.

Reference

  1. ^ Kwiatkowska, M.; Norman, G .; Parker, D. (2011). „PRISM 4.0: Ověření pravděpodobných systémů v reálném čase“. v Proc. 23. mezinárodní konference o ověřování pomocí počítače (CAV’11), svazek 6806 přednášek v informatice, strany 585-591, Springer.
  2. ^ Kwiatkowska, M .; Norman, G .; Parker, D. "Ověření pravděpodobnostního modelu v praxi: Případové studie s PRISM". Hodnocení vyhodnocení výkonu ACM SIGMETRICS, 32 (4), strany 16–21.

externí odkazy