Conjunto de herramientas de análisis estático de software MALPAS

MALPAS es un conjunto de herramientas de software que permite investigar y comprobar la corrección del software mediante un análisis estático riguroso de programas . La herramienta utiliza grafos dirigidos y álgebra regular para representar el programa analizado. Mediante las herramientas automatizadas de MALPAS, un analista puede describir la estructura de un programa, clasificar el uso de los datos y establecer las relaciones de información entre los datos de entrada y salida. Además, permite realizar una prueba formal de que el código cumple con sus especificaciones.

MALPAS se ha utilizado para confirmar la corrección de aplicaciones críticas para la seguridad en las industrias nuclear, ^{[ 1 ]} aeroespacial ^{[ 2 ]} y de defensa ^{[ 3 ]} . También se ha utilizado para proporcionar corrección del compilador en la industria nuclear en Sizewell B . ^{[ 4 ]} Los lenguajes que se han analizado incluyen: Ada , C , PLM e Intel Assembler .

MALPAS es muy adecuado para el análisis estático independiente requerido por la guía del Ejecutivo de Salud y Seguridad del Reino Unido para sistemas de protección basados ​​en computadora para reactores nucleares debido a su rigor y flexibilidad para manejar muchos lenguajes de programación. ^{[ 5 ]}

El conjunto de herramientas MALPAS comprende cinco herramientas de análisis específicas que abordan diversas propiedades de un programa. La entrada a los analizadores debe estar escrita en el Lenguaje Intermedio (LI) de MALPAS; este puede escribirse manualmente o generarse mediante una herramienta de traducción automática a partir del código fuente original. Existen traductores automáticos para lenguajes de programación de alto nivel comunes como Ada , C y Pascal , así como para lenguajes ensamblador como Intel 80*86 , PowerPC y 68000. El texto LI se introduce en MALPAS a través del "Lector LI", que construye un grafo dirigido y la semántica asociada para el programa analizado. El grafo se reduce mediante una serie de técnicas de reducción de grafos.

El conjunto de herramientas MALPAS consta de 5 analizadores: ^{[ 6 ]}

1. Analizador de flujo de control. Este analizador examina la estructura del programa, identificando características clave: puntos de entrada/salida, bucles, bifurcaciones y código inaccesible. Proporciona un informe resumido que resalta las estructuras no deseadas e indica la complejidad del programa.
2. Analizador de uso de datos. Este analizador clasifica las variables y los parámetros utilizados por el programa en distintas categorías según su uso (por ejemplo, datos que se leen antes de escribirse, datos que se escriben sin leerse previamente o datos que se escriben dos veces sin una lectura intermedia). El informe puede identificar errores como datos no inicializados y salidas de funciones que no se escriben en todas las rutas.
3. Analizador de flujo de información . Este analizador identifica las dependencias de datos y de ramificación para cada variable o parámetro de salida. Permite detectar dependencias no deseadas o inesperadas en todas las rutas del código. También proporciona información sobre variables no utilizadas e instrucciones redundantes.
4. Analizador semántico (también conocido como ejecución simbólica ). Este método revela la relación funcional exacta entre todas las entradas y salidas a lo largo de todas las rutas semánticamente posibles del código.
5. Analizador de Conformidad. Este analizador compara el comportamiento matemático del código con su especificación IL formal, detallando las diferencias entre ambas. La especificación IL se presenta en forma de precondiciones y postcondiciones , además de aserciones de código opcionales. El análisis de conformidad permite obtener un alto grado de confianza en la corrección funcional del código con respecto a su especificación.

La investigación original y las primeras versiones del conjunto de herramientas fueron creadas por el Royal Signals and Radar Establishment (RSRE) del Reino Unido en Malvern, Inglaterra (de ahí el nombre, MALvern Programming Analysis Suite). Se utilizó ampliamente en el ámbito nuclear civil y de armamento en la década de 1980, cuando contó con el apoyo de Rex, Thompson and Partners, que creó el Grupo de Usuarios de MALPAS, cuyo primer presidente fue David H Smith (actualmente en Frazer-Nash), y posteriormente por Advantage Technical Consulting (adquirida por Atkins en 2008).

La primera tarea de análisis estático a gran escala se centró en el sistema de protección del reactor primario de la central eléctrica Sizewell B. Esta fue la primera central nuclear del Reino Unido en emplear un sistema de protección basado en computadora como primera línea de defensa contra una falla catastrófica. Además, CEZ en la República Checa empleó MALPAS para aumentar la confianza en el sistema de protección del reactor en la central nuclear de Temelin . En 1995, la Real Fuerza Aérea del Reino Unido encargó un análisis independiente del software de aviónica del Lockheed Martin C130J , considerado crítico para la seguridad. MALPAS se utilizó para el análisis de este software, además del software del ordenador de misión, que fue escrito en Spark Ada y verificado con Spark Toolset. ^{[ 7 ]} Actualmente, MALPAS se está utilizando para evaluar de forma independiente el software del sistema de protección del reactor que supervisará los dos reactores nucleares en Hinkley Point C. ^{[ 8 ]}