PRISM es un verificador de modelos probabilísticos , una herramienta de software de verificación formal para el modelado y análisis de sistemas que exhiben un comportamiento probabilístico. [1] PRISM se introdujo alrededor de 2002 en el contexto del trabajo de doctorado de Parker y todavía se encuentra en desarrollo activo (a partir de 2024).
Una fuente de estos sistemas es el uso de la aleatorización , por ejemplo en protocolos de comunicación como Bluetooth y FireWire , o en protocolos de seguridad como Crowds y Onion Routing . El comportamiento estocástico también surge en muchos otros sistemas informáticos, por ejemplo debido a fallos de los equipos, sensores y actuadores poco fiables o retrasos impredecibles en las comunicaciones. PRISM se ha utilizado para analizar una amplia gama de aplicaciones, desde la planificación de robots hasta el análisis del rendimiento de redes informáticas y redes de reacciones bioquímicas . [2]
PRISM se puede utilizar para analizar varios tipos diferentes de modelos probabilísticos, incluidas las cadenas de Markov de tiempo discreto , las cadenas de Markov de tiempo continuo , los procesos de decisión de Markov y las extensiones probabilísticas del formalismo de autómatas cronometrados . También admite modelos probabilísticos con observabilidad parcial y nociones de incertidumbre epistémica. Las propiedades que se deben verificar frente a estos modelos se expresan en extensiones probabilísticas de lógica temporal , como PCTL . La herramienta complementaria de PRISM, PRISM-games [3], proporciona análisis para juegos estocásticos .
El desarrollo de PRISM está dirigido por la Universidad de Oxford . El proyecto comenzó originalmente en la Universidad de Birmingham . La herramienta es un software de código abierto , publicado bajo la Licencia Pública General de GNU . PRISM ha sido seleccionado para el programa Google Summer of Code en 2013 y 2014. La herramienta y sus creadores han ganado varios premios: el premio ETAPS Test-of-Time Tool Award 2024 y el premio HVC 2016.
El verificador de modelos probabilísticos PRISM parece no estar relacionado con el sistema de programación lógica probabilística PRISM (PRogramming In Statistical Modelling, introducido a fines de la década de 1990 por Sato y colaboradores).