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 estático de programas . La herramienta utiliza gráficos dirigidos y álgebra regular para representar el programa bajo análisis. Utilizando las herramientas automatizadas de 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 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 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 diversas propiedades de un programa. La entrada a los analizadores debe estar escrita en MALPAS Intermediate Language (IL); esto puede estar escrito a mano o producido mediante una herramienta de traducción automática a partir del código fuente original. Existen traductores automáticos para lenguajes de programación comunes de alto nivel como Ada , C y Pascal , así como 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 dirigido y la semántica asociada para el programa bajo análisis. El gráfico se reduce utilizando una serie de técnicas de reducción de gráficos.
El conjunto de herramientas MALPAS consta de 5 analizadores: [6]
La investigación original y las generaciones iniciales del conjunto de herramientas fueron creadas por 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 las armas nucleares y civiles en la década de 1980, cuando contó con el apoyo de Rex, Thompson and Partners, quienes crearon el Grupo de Usuarios MALPAS, cuyo primer presidente fue David H Smith (ahora de Frazer-Nash) y luego, posteriormente, Advantage Technical Consulting (comprada por Atkins en 2008).
La primera tarea de análisis estático a gran escala tuvo lugar 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 que empleó un sistema de protección informático como primera línea de defensa contra un fallo catastrófico. Además, CEZ en la República Checa utilizó MALPAS para aumentar la confianza en el sistema de protección del reactor de la central nuclear de Temelin . En 1995, la Royal Air Force del Reino Unido encargó un análisis independiente del software de aviónica del Lockheed Martin C130J 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] MALPAS se está utilizando actualmente para evaluar de forma independiente el software para el sistema de protección del reactor que monitoreará los dos reactores nucleares en Hinkley Point C. [8]
{{cite web}}: Mantenimiento CS1: copia archivada como título ( enlace )