Model checking probabilístico: avances y aplicaciones
Los sistemas informáticos desempeñan un rol importante en casi todos los aspectos de la vida cotidiana, incluyendo muchos ejemplos donde la seguridad y confiabilidad son críticas, desde el control de sistemas para vehículos autónomos hasta embeber software médico en dispositivos como un marca-pasos cardíaco. Por lo tanto, existe una demanda de rigurosas técnicas formales que puedan verificar que esos sistemas funcionan correctamente y seguramente. A menudo, esto requiere un análisis de aspectos cuantitativos como confiabilidad, responsividad y el uso de recursos. Además, dado que estos dispositivos operan en ambientes impredecibles y desconocidos es esencial considerar la naturaleza inherente probabilística de los sistemas reales, como la sincronización aleatoria de eventos, fallas de componentes embebidos y la pérdida de paquetes cuando se usa redes de comunicación inalámbrica.
Este post es una traducción de Probabilistic Model Checking: Advances and Applications
Model Checking probabilístico es una técnica automática para la verificación formal de propiedades cuantitativas de sistemas estocásticos. Esto involucra la construcción de un modelo matemático que represente el comportamiento de un sistema a través del tiempo, es decir los posibles estados en los que puede estar, las transiciones que pueden ocurrir entre estados e información sobre la probabilidad o el momento de estas transiciones. Las propiedades que especifican el comportamiento requerido de estos sistemas son luego formalmente especificados en lógica temporal y luego se realiza una exploración y análisis semánticos del modelo del sistema para determinar si las propiedades están propiedades están satisfechas.
Model Checking probabilístico es una técnica automática para la verificación formal de propiedades cuantitativas de sistemas estocásticos.
Este enfoque permite una amplia variedad de propiedades cuantitativas a ser especificadas, por ejemplo, “la probabilidad de que ocurra una falla en un sistema”, “la probabilidad de que un paquete sea exitosamente entregado dentro de 5ms” o “el consumo de energía esperado de una red de sensores durante 1h de operación”. La teoría básica y los algoritmos para model checking probabilístico se presentaron por primera vez en la década de 1980 pero, desde entonces, sustanciales progresos han sido hechos en el desarrollo de la teoría, algoritmos y herramientas para diferentes tipos de modelos probabilísticos y una amplia gama de especificación de propiedades. Esto ha resultado en el uso exitoso de model checking probabilístico en una amplia gama de sistemas computarizados, desde controladores de bolsas de aire hasta marcapasos cardíacos, y en una amplia gama de dominios de aplicaciones, desde seguridad informática hasta robótica y computación cuántica.
La teoría básica y los algoritmos para model checking probabilístico se presentaron por primera vez en la década de 1980.
El objetivo de este capítulo es proporcionar una introducción a los conceptos básicos de model checking probabilístico y un resumen de algunos de los avances clave que se han realizado en los últimos años. En ambos casos, ilustraremos las ideas usando una variedad de ejemplos de juguetes y casos de estudio de la vida real, y proporcionar sugerencias para futuros trabajos y recursos. También pondremos disponible copias electrónicas de los archivos correspondientes al estudio de estos ejemplos y casos de estudio usando el model checker PRISM.
- Título Original: Probabilistic Model Checking: Advances and Applications
- Autores: Marta Kwiatkowska, Gethin Norman y David Parker
- Año: 2018
- Libro: Sistemas de verificación formal/ Formal system verification
- Capítulo: 3
Estructura del artículo
En la primera sección del capítulo, daremos una introducción de model checking probabilístico aplicado a diferentes tipos de modelos: cadenas de markov discretas, procesos de decisión de markov y juegos estocásticos multijugador. Luego pasamos a cubrir una sección de temas más avanzados. Esto incluye: (i) síntesis del controlador, que se puede usar para generar controladores correctos por construcción, por ejemplo, para robots o vehículos, junto con garantías cuantitativas sobre su comportamiento; (ii) técnicas de modelado y verificación diseñadas para sistemas grandes y complejos, incluidos los enfoques de composición (dividir y conquistar) y el uso de la abstracción; (iii) técnicas de verificación para modelos probabilísticos en tiempo real, es decir, aquellos que capturan información más realista sobre el tiempo y la duración de los eventos del sistema; y (iv) métodos paramétricos de model checking, que proporcionan formas más potentes para analizar modelos cuyos parámetros (por ejemplo, probabilidades) pueden variar o ser difíciles de cuantificar con precisión. Concluimos el capítulo con una discusión sobre las limitaciones de model checking probabilístico y algunos de los actuales desafíos clave y las direcciones de investigación.
