Resumen

Uno de los principales desafíos en la verificación formal del software de sistemas empotrados es la complejidad y el tamaño sustancialmente grande de la implementación. El problema se vuelve crucial cuando el sistema empotrado es un dispositivo médico complejo que ejecuta algoritmos enrevesados. En la verificación basada en refinamiento, tanto la especificación como la implementación se expresan como sistemas de transición. Cada comportamiento del sistema de transición de la implementación se corresponde con el sistema de transición de la especificación con la ayuda de un mapa de refinamiento. El mapa de refinamiento solo puede proyectar aquellos valores de la implementación que son responsables de etiquetar el estado actual del sistema. Cuando el mapa de refinamiento se aplica a nivel de código objeto, numerosas instrucciones se corresponden con un solo estado en el sistema de transición de la especificación llamado instrucciones de tartamudeo. Utilizamos el concepto de Abstracción de Tartamudeo Estático (SSA) que filtra los múltiples segmentos comunes de instrucciones de tartamudeo y reemplaza cada segment

• Materias:Big Data Segmentación de líneas Tráfico de red Reconocimiento de entidad Esquema de programación
• Subjects:Big Data Line segmentation Network traffic Entity recognition Programming scheme
• Palabras claves:Principales desafíos; Verificación formal; Software de sistemas embebidos; Complejidad; Implementación; Abstracción Estática de Tartamudeo (SSA)
• Keywords:Major challenges; Formal verification; Embedded system software; Complexity; Implementation; Static Stuttering Abstraction (SSA)