MALPAS

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

Graph (mathematics)

In mathematics, a graph is an abstract representation of a set of objects where some pairs of the objects are connected by links. The interconnected objects are represented by mathematical abstractions called vertices, and the links that connect some pairs of vertices are called edges...

 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

Formal proof

A formal proof or derivation is a finite sequence of sentences each of which is an axiom or follows from the preceding sentences in the sequence by a rule of inference. The last sentence in the sequence is a theorem of a formal system...

 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

Compiler

A compiler is a computer program that transforms source code written in a programming language into another computer language...

 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

Health and Safety Executive

The Health and Safety Executive is a non-departmental public body in the United Kingdom. It is the body responsible for the encouragement, regulation and enforcement of workplace health, safety and welfare, and for research into occupational risks in England and Wales and Scotland...

 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

Ada (programming language)

Ada is a structured, statically typed, imperative, wide-spectrum, and object-oriented high-level computer programming language, extended from Pascal and other languages...

, C

C (programming language)

C is a general-purpose computer programming language developed between 1969 and 1973 by Dennis Ritchie at the Bell Telephone Laboratories for use with the Unix operating system....

 and Pascal

Pascal (programming language)

Pascal is an influential imperative and procedural programming language, designed in 1968/9 and published in 1970 by Niklaus Wirth as a small and efficient language intended to encourage good programming practices using structured programming and data structuring.A derivative known as Object Pascal...

, as well as assembler languages such as Intel 80*86

X86 assembly language

x86 assembly language is a family of backward-compatible assembly languages, which provide some level of compatibility all the way back to the Intel 8008. x86 assembly languages are used to produce object code for the x86 class of processors, which includes Intel's Core series and AMD's Phenom and...

, PowerPC

PowerPC

PowerPC is a RISC architecture created by the 1991 Apple–IBM–Motorola alliance, known as AIM...

 and 68000. The IL text is input into MALPAS via the "IL Reader", which constructs a directed graph

Directed graph

A directed graph or digraph is a pair G= of:* a set V, whose elements are called vertices or nodes,...

 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:

1. Control Flow Analyser. This examines the program structure, identifying key features: Entry/Exit points, Loops, Branches and unreachable code. It provides a summary report drawing attention to undesirable constructs and an indication of the complexity of the program structure.
2. Data Use Analyser. This separates the variables and parameters used by the program into distinct classes depending upon their use. (ie Data that is read before being written, Data that is written without being read or Data that is written twice without an intervening read). The report can identify errors such as uninitialised data and function outputs not written on all paths.
3. Information Flow Analyser
   Data-flow analysis
   Data-flow analysis is a technique for gathering information about the possible set of values calculated at various points in a computer program. A program's control flow graph is used to determine those parts of a program to which a particular value assigned to a variable might propagate. The...
   
   . This identifies the data and branch dependencies for each output variable or parameter. Unwanted or unexpected dependencies can be revealed for all paths through the code. Information is also provided regarding unused variables and redundant statements.
4. Semantic Analyser (also known as symbolic execution
   Symbolic execution
   In computer science, symbolic execution refers to the analysis of programs by tracking symbolic rather than actual values, a case of abstract interpretation. The field of symbolic simulation applies the same concept to hardware...
   
   ). This reveals the exact functional relationship between all inputs and outputs over all semantically-feasible paths through the code.
5. Compliance Analyser. This compares the mathematical behaviour of the code with its formal IL specification, detailing where one differs from the other. The IL specification is written as Precondition
   Precondition
   In computer programming, a precondition is a condition or predicate that must always be true just prior to the execution of some section of code or before an operation in a formal specification....
   
   s and Postcondition
   Postcondition
   In computer programming, a postcondition is a condition or predicate that must always be true just after the execution of some section of code or after an operation in a formal specification. Postconditions are sometimes tested using assertions within the code itself...
   
   s, as well as optional code assertions. Compliance analysis can be used to gain a very high level of confidence in the functional correctness of the code in relation to its specification.

History

The original research and initial generations of the toolset were created by the UK's Royal Signals and Radar Establishment

Royal Signals and Radar Establishment

The Royal Signals and Radar Establishment was a scientific research establishment within the Ministry of Defence of the United Kingdom, located primarily at Malvern in Worcestershire. It was formed in 1976 in an amalgamation of earlier research establishments including the Royal Radar Establishment...

 (RSRE) in Malvern, England (hence the derivation of the name, MALvern Programming Analysis Suite). It was used here in a purely research capacity before being employed commercially 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

CEZ Group

CEZ Group is a conglomerate of 96 companies , 72 of them in the Czech Republic. It is involved in the electricity generation, distribution, and trade. CEZ Group operates also in Albania, Austria, Bosnia and Herzegovina, Bulgaria, Germany, Hungary, Kosovo, Poland, Romania, Serbia, Slovakia and...

 in the Czech Republic employed MALPAS to increase the confidence in the reactor protection system in the Temelin Nuclear Power Station

Temelín Nuclear Power Station

Temelín Nuclear Power Station is located near Temelín, a small village in the Czech Republic. Temelín NPP is owned by ČEZ Group, which employs 1000 workers at this site. The adjacent castle Vysoký Hrádek serves as an information centre.-History:...

. Other examples of high integrity software scrutinized using MALPAS include C130J engine control system.