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 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.[5]
Technical Overviewedit
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.
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). 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.
Historyedit
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 MartinC130J'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.[7] 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.[8]
^Formal demonstration of equivalence of source code and PROM contents, Proceedings of the IMA Conference on Mathematics of Dependable Systems, Oxford University Press, 1995, pp225248D J Pavey and L A Winsborrow
^Industrial Perspective on Static Analysis. Software Engineering Journal Mar. 1995: 69-75Wichmann, B. A., A. A. Canning, D. L. Clutterbuck, L. A. Winsbarrow, N. J. Ward, and D. W. R. Marsh. http://www.ida.liu.se/~TDDC90/papers/industrial95.pdf
^Static Code Analysis on the C-130J Hercules Safety-Critical Software (PDF). Archived from the original (PDF) on 2011-09-27. Retrieved 2011-03-18.{{cite web}}: CS1 maint: archived copy as title (link)
malpas, software, static, analysis, toolset, malpas, software, toolset, that, provides, means, investigating, proving, correctness, software, applying, rigorous, form, static, program, analysis, tool, uses, directed, graphs, regular, algebra, represent, progra. 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 Developer s AtkinsOperating systemWindowsTypeStatic program analysisLicenseProprietaryWebsitewww wbr malpas global wbr comMALPAS has been used to confirm the correctness of safety critical applications in the nuclear 1 aerospace 2 and defence 3 industries It has also been used to provide compiler correctness in the nuclear industry on Sizewell B 4 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 5 Technical Overview editThe 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 6 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 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 editThe 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 7 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 8 References edit Programmable Protection in UK NPP 10 years on D Pavey British Energy http entrac iaea org I and C TM VTT 2005 11 IAEA papers 051124 Thursday IAEA paper Pavey pdf Static Code Analysis on the C 130J Hercules Safety Critical Software Eur Ing K J Harrison BSc CPhys MinstP CEng MRAeS MBCS Aerosystems International UK PDF Archived from the original PDF on 2011 09 27 Retrieved 2011 03 18 An analysis of ordnance software using the MALPAS tools Hayman K Defence Sci amp Technol Organ Salisbury SA http www dsto defence gov au publications scientific record php record 9074 Formal demonstration of equivalence of source code and PROM contents Proceedings of the IMA Conference on Mathematics of Dependable Systems Oxford University Press 1995 pp225248D J Pavey and L A Winsborrow Computer based safety systems technical guidance for assessing software aspects of digital computer based protection systems Archived from the original on 2011 07 04 Industrial Perspective on Static Analysis Software Engineering Journal Mar 1995 69 75Wichmann B A A A Canning D L Clutterbuck L A Winsbarrow N J Ward and D W R Marsh http www ida liu se TDDC90 papers industrial95 pdf Static Code Analysis on the C 130J Hercules Safety Critical Software Archived copy PDF Archived from the original PDF on 2011 09 27 Retrieved 2011 03 18 a href Template Cite web html title Template Cite web cite web a CS1 maint archived copy as title link https www newcivilengineer com latest atkins wins hinkley point c safety contract 27 04 2020 Retrieved from https en wikipedia org w index php title MALPAS Software Static Analysis Toolset amp oldid 1165630480, wikipedia, wiki, book, books, library,
