MALPAS Software Static Analysis Toolset
MALPAS is a software toolset that provides a means of investigating and proving the correctness of software by applying a rigorous form of static program analysis. The tool uses directed graphs and regular algebra to represent the program under analysis. Using the automated tools in MALPAS an analyst can describe the structure of a program, classify the use made of data and provide the information relationships between input and output data. It also supports a formal proof that the code meets its specification. MALPAS has been used to confirm the correctness of safety critical applications  in the nuclear, aerospace and defence industries. It has also been used to provide compiler validation in the nuclear industry on Sizewell B. Languages that have been analysed include: Ada, C, PLM and Intel Assembler. MALPAS is well suited to the independent static analysis required by the UK's Health and Safety Executive guidance for computer based protection systems for nuclear reactors due to its rigour and flexibility in handling many programming languages. Technical Overview. The MALPAS toolset comprises five specific analysis tools that address various properties of a program. The input to the analysers needs to be written in  MALPAS Intermediate Language (IL); this can be hand-written or produced by an automated translation tool from the original source code. Automatic translators exist for common high-level programming languages such as Ada, C and Pascal, as well as assembler languages such as Intel 80*86, PowerPC and 68000. The IL text is input into MALPAS via the "IL Reader", which constructs a directed graph and associated semantics for the program under analysis. The graph is reduced using a series of graph reduction techniques. The MALPAS toolset consists of 5 analysers: History. The original research and initial generations of the  toolset were created by the UK's Royal Signals and Radar Establishment (RSRE) in Malvern, England (hence the derivation of the name, MALvern Programming Analysis Suite). It was used extensively in the civil nuclear and weapons field in the 1980s, when it was supported by Rex, Thompson and Partners, who set up the MALPAS User Group, with the first chair being David H Smith (now of Frazer-Nash) and then subsequently by Advantage Technical Consulting (bought by Atkins in 2008). The first large scale static analysis task was on the primary reactor protection system for the Sizewell B power station . This was the UK's first nuclear power station to employ a computer-based protection system as its first line of defence against a catastrophic failure. Further to this, CEZ in the Czech Republic employed MALPAS to increase the confidence in the reactor protection system in the Temelin Nuclear Power Station. In 1995 the UK's Royal Air Force commissioned independent analysis of the Lockheed Martin C130J's avionics software assessed as safety-critical. MALPAS was used for the analysis of this software, apart from the Mission Computer software, which was written in Spark Ada and verified with the Spark  Toolset.