Verificación de Ejecución Centrada en Datos de Sistemas Ciberfísicos Médicos Inalámbricos

Los sistemas ciberfísicos médicos inalámbricos son ampliamente adoptados en las prácticas diarias de la medicina, donde grandes cantidades de datos son muestreados por dispositivos médicos inalámbricos y sensores, y se transmiten a los sistemas de apoyo a la decisión (SAD). Se han codificado muchas guías basadas en texto para la simulación del flujo de trabajo de SAD para automatizar la atención médica basada en los datos recolectados. Pero para algunas enfermedades complejas y críticas para la vida, es altamente deseable verificar automáticamente y de manera rigurosa algunas propiedades temporales complejas codificadas en esos datos, lo que plantea nuevos desafíos para los SAD actuales, que tienen un soporte limitado para la verificación formal automática y el análisis de datos en tiempo real. En este artículo, realizamos el primer estudio sobre la aplicación de la verificación en tiempo de ejecución para cooperar con los SAD actuales basados en datos en tiempo real. Dentro de la técnica propuesta, se ha diseñado un lenguaje específico de dominio fácil de usar, llamado DRTV, para especificar datos vitales en tiempo real muestreados por dispositivos médicos y propiedades temporales originadas de guías clínicas. Se han desarrollado algunas interfaces para la adquisición y comunicación de datos. Luego, para los escenarios de práctica médica descritos en el modelo DRTV, generaremos automáticamente secuencias de eventos y autómatas verificadores de propiedades en tiempo de ejecución. Si una propiedad temporal se viola, se producirán advertencias en tiempo real por el verificador formal y se enviarán al SAD médico. Hemos utilizado DRTV para especificar diferentes tipos de escenarios de atención médica y hemos aplicado la técnica propuesta para ayudar al sistema ciberfísico médico inalámbrico existente. Como se presenta en los resultados del experimento, en términos de detección de advertencias, supera el uso único de SAD o la inspección humana, y mejora la calidad de la atención médica clínica del hospital.