MALPAS es un conjunto de herramientas de software que proporciona un medio para investigar y probar la corrección del software mediante la aplicación de una forma rigurosa de análisis de programa estático . La herramienta utiliza gráficos dirigidos y álgebra regular para representar el programa bajo análisis. Usando las herramientas automatizadas en MALPAS, un analista puede describir la estructura de un programa, clasificar el uso que se hace de los datos y proporcionar las relaciones de información entre los datos de entrada y salida. También admite una prueba formal de que el código cumple con su especificación.
MALPAS se ha utilizado para confirmar la exactitud de las aplicaciones críticas para la seguridad en las industrias nuclear, [1] aeroespacial [2] y de defensa [3] . También se ha utilizado para proporcionar compilador de validación en la industria nuclear de Sizewell B . [4] Los idiomas que se han analizado incluyen: Ada , C , PLM e Intel Assembler .
MALPAS se adapta bien al análisis estático independiente requerido por la guía Ejecutiva de Salud y Seguridad del Reino Unido para sistemas de protección basados en computadora para reactores nucleares debido a su rigor y flexibilidad en el manejo de muchos lenguajes de programación. [5]
El conjunto de herramientas MALPAS comprende cinco herramientas de análisis específicas que abordan varias propiedades de un programa. La entrada a los analizadores debe escribirse en MALPAS Intermediate Language (IL); esto puede ser escrito a mano o producido por 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 ensambladores como Intel 80 * 86 , PowerPC y 68000 . El texto IL se ingresa en MALPAS a través del "IL Reader", que construye un gráfico dirigidoy semántica asociada para el programa bajo análisis. El gráfico se reduce mediante una serie de técnicas de reducción de gráficos.
La investigación original y las generaciones iniciales del conjunto de herramientas fueron creadas por el Royal Signals and Radar Establishment (RSRE) del Reino Unido en Malvern, Inglaterra (de ahí la derivación del nombre, MALvern Programming Analysis Suite). Se utilizó ampliamente en el campo de armas y armas nucleares civiles en la década de 1980, cuando fue apoyado por Rex, Thompson and Partners, quienes establecieron el Grupo de Usuarios de MALPAS, siendo el primer presidente David H Smith (ahora de Frazer-Nash) y luego, posteriormente, por Advantage Technical Consulting (comprado por Atkins en 2008).
La primera tarea de análisis estático a gran escala fue en el sistema de protección del reactor primario para 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 su primera línea de defensa contra una falla catastrófica. Además de esto, CEZ en la República Checa utilizó MALPAS para aumentar la confianza en el sistema de protección del reactor en la Central Nuclear de Temelin . En 1995, la Royal Air Force del Reino Unido encargó un análisis independiente del Lockheed Martin C130JEl software de aviónica evaluado como crítico para la seguridad. Para el análisis de este software se utilizó MALPAS, además del software Mission Computer, que fue escrito en Spark Ada y verificado con Spark Toolset. [7]