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
In mathematics, a Kleene algebra ( ; named after Stephen Cole Kleene) is an idempotent (and thus partially ordered) semiring endowed with a closure operator. It generalizes the operations known from regular expressions.
Definition
Various ine ...
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
In logic and mathematics, a formal proof or derivation is a finite sequence of sentences (called well-formed formulas in the case of a formal language), each of which is an axiom, an assumption, or follows from the preceding sentences in the seque ...
that the code meets its specification.
MALPAS has been used to confirm the correctness of
safety critical
A safety-critical system (SCS) or life-critical system is a system whose failure or malfunction may result in one (or more) of the following outcomes:
* death or serious injury to people
* loss or severe damage to equipment/property
* environme ...
applications in the nuclear, aerospace and defence industries. It has also been used to provide
compiler correctness in the nuclear industry on
Sizewell B
The Sizewell nuclear site consists of two nuclear power stations, one of which is still operational, located near the small fishing village of Sizewell in Suffolk, England. Sizewell A, with two Magnox reactors, is now in the process of being dec ...
. Languages that have been analysed include:
Ada
Ada may refer to:
Places
Africa
* Ada Foah, a town in Ghana
* Ada (Ghana parliament constituency)
* Ada, Osun, a town in Nigeria
Asia
* Ada, Urmia, a village in West Azerbaijan Province, Iran
* Ada, Karaman, a village in Karaman Province, Tur ...
,
C,
PLM and
Intel Assembler.
MALPAS is well suited to the independent static analysis required by the UK's
Health and Safety Executive
The Health and Safety Executive (HSE) is a UK government agency responsible for the encouragement, regulation and enforcement of workplace health, safety and welfare, and for research into occupational risks in Great Britain. It is a non-depar ...
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 may refer to:
Places
Africa
* Ada Foah, a town in Ghana
* Ada (Ghana parliament constituency)
* Ada, Osun, a town in Nigeria
Asia
* Ada, Urmia, a village in West Azerbaijan Province, Iran
* Ada, Karaman, a village in Karaman Province, Tur ...
,
C and
Pascal
Pascal, Pascal's or PASCAL may refer to:
People and fictional characters
* Pascal (given name), including a list of people with the name
* Pascal (surname), including a list of people and fictional characters with the name
** Blaise Pascal, Fren ...
, as well as assembler languages such as
Intel 80*86,
PowerPC
PowerPC (with the backronym Performance Optimization With Enhanced RISC – Performance Computing, sometimes abbreviated as PPC) is a reduced instruction set computer (RISC) instruction set architecture (ISA) created by the 1991 Apple Inc., App ...
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:
# 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.
# Data Use Analyser. This separates the variables and parameters used by the program into distinct classes depending upon their use. (i.e. 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.
#
Information Flow Analyser. 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.
# Semantic Analyser (also known as
symbolic execution In computer science, symbolic execution (also symbolic evaluation or symbex) is a means of analyzing a program to determine what inputs cause each part of a program to execute. An interpreter follows the program, assuming symbolic values for inp ...
). This reveals the exact functional relationship between all inputs and outputs over all semantically-feasible paths through the code.
# 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
Preconditions and
Postconditions, 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 (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 Atkins may refer to:
Places in the United States
* Atkins, Arkansas, a city
* Atkins, Iowa, a city
* Atkins, Louisiana, an unincorporated community
* Atkins, Nebraska, an unincorporated community
* Atkins, Virginia, a census-designated place
* ...
in 2008).
The first large scale static analysis task was on the primary reactor protection system for the
Sizewell B
The Sizewell nuclear site consists of two nuclear power stations, one of which is still operational, located near the small fishing village of Sizewell in Suffolk, England. Sizewell A, with two Magnox reactors, is now in the process of being dec ...
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
The Royal Air Force (RAF) is the United Kingdom's air and space force. It was formed towards the end of the First World War on 1 April 1918, becoming the first independent air force in the world, by regrouping the Royal Flying Corps (RFC) and ...
commissioned independent analysis of the
Lockheed Martin
The Lockheed Martin Corporation is an American aerospace, arms, defense, information security, and technology corporation with worldwide interests. It was formed by the merger of Lockheed Corporation with Martin Marietta in March 1995. It ...
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.
MALPAS is currently being used to independently assess the software for the reactor protection system which will monitor the two nuclear reactors at Hinkley Point C.
[https://www.newcivilengineer.com/latest/atkins-wins-hinkley-point-c-safety-contract-27-04-2020/]
References
{{reflist
Formal methods tools
Software testing tools
Theorem proving software systems
Model checkers
Static program analysis tools