MALPAS Software Static Analysis Toolset

Last updated
Developer(s) Atkins
Operating system Windows
Type Static program analysis
License Proprietary
Website www.malpas-global.com

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.

Contents

MALPAS 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

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: [6]

  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. (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.
  3. 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.
  4. 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.
  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 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 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]

Related Research Articles

In computer science, static program analysis is the analysis of computer programs performed without executing them, in contrast with dynamic program analysis, which is performed on programs during their execution.

In computer science, program analysis is the process of automatically analyzing the behavior of computer programs regarding a property such as correctness, robustness, safety and liveness. Program analysis focuses on two major areas: program optimization and program correctness. The first focuses on improving the program’s performance while reducing the resource usage while the latter focuses on ensuring that the program does what it is supposed to do.

<span class="mw-page-title-main">State diagram</span> Diagram of behavior of finite state systems

A state diagram is a type of diagram used in computer science and related fields to describe the behavior of systems. State diagrams require that the system described is composed of a finite number of states; sometimes, this is indeed the case, while at other times this is a reasonable abstraction. Many forms of state diagrams exist, which differ slightly and have different semantics.

<span class="mw-page-title-main">Safety-critical system</span> System whose failure would be serious

A safety-critical system (SCS) or life-critical system is a system whose failure or malfunction may result in one of the following outcomes:

Avionics software is embedded software with legally mandated safety and reliability concerns used in avionics. The main difference between avionic software and conventional embedded software is that the development process is required by law and is optimized for safety. It is claimed that the process described below is only slightly slower and more costly than the normal ad hoc processes used for commercial software. Since most software fails because of mistakes, eliminating the mistakes at the earliest possible step is also a relatively inexpensive and reliable way to produce software. In some projects however, mistakes in the specifications may not be detected until deployment. At that point, they can be very expensive to fix.

<span class="mw-page-title-main">Model checking</span> Computer science field

In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification. This is typically associated with hardware or software systems, where the specification contains liveness requirements as well as safety requirements.

<span class="mw-page-title-main">Race condition</span> When a systems behavior depends on timing of uncontrollable events

A race condition or race hazard is the condition of an electronics, software, or other system where the system's substantive behavior is dependent on the sequence or timing of other uncontrollable events. It becomes a bug when one or more of the possible behaviors is undesirable.

In computing, dataflow is a broad concept, which has various meanings depending on the application and context. In the context of software architecture, data flow relates to stream processing or reactive programming.

In computer programming, dataflow programming is a programming paradigm that models a program as a directed graph of the data flowing between operations, thus implementing dataflow principles and architecture. Dataflow programming languages share some features of functional languages, and were generally developed in order to bring some functional concepts to a language more suitable for numeric processing. Some authors use the term datastream instead of dataflow to avoid confusion with dataflow computing or dataflow architecture, based on an indeterministic machine paradigm. Dataflow programming was pioneered by Jack Dennis and his graduate students at MIT in the 1960s.

<span class="mw-page-title-main">Singularity (operating system)</span> Experimental operating system from Microsoft Research

Singularity is an experimental operating system developed by Microsoft Research between July 9, 2003, and February 7, 2015. It was designed as a high dependability OS in which the kernel, device drivers, and application software were all written in managed code. Internal security uses type safety instead of hardware memory protection.

Runtime verification is a computing system analysis and execution approach based on extracting information from a running system and using it to detect and possibly react to observed behaviors satisfying or violating certain properties. Some very particular properties, such as datarace and deadlock freedom, are typically desired to be satisfied by all systems and may be best implemented algorithmically. Other properties can be more conveniently captured as formal specifications. Runtime verification specifications are typically expressed in trace predicate formalisms, such as finite state machines, regular expressions, context-free patterns, linear temporal logics, etc., or extensions of these. This allows for a less ad-hoc approach than normal testing. However, any mechanism for monitoring an executing system is considered runtime verification, including verifying against test oracles and reference implementations. When formal requirements specifications are provided, monitors are synthesized from them and infused within the system by means of instrumentation. Runtime verification can be used for many purposes, such as security or safety policy monitoring, debugging, testing, verification, validation, profiling, fault protection, behavior modification, etc. Runtime verification avoids the complexity of traditional formal verification techniques, such as model checking and theorem proving, by analyzing only one or a few execution traces and by working directly with the actual system, thus scaling up relatively well and giving more confidence in the results of the analysis, at the expense of less coverage. Moreover, through its reflective capabilities runtime verification can be made an integral part of the target system, monitoring and guiding its execution during deployment.

<span class="mw-page-title-main">Call graph</span> Structure in computing

A call graph is a control-flow graph, which represents calling relationships between subroutines in a computer program. Each node represents a procedure and each edge (f, g) indicates that procedure f calls procedure g. Thus, a cycle in the graph indicates recursive procedure calls.

<span class="mw-page-title-main">Structured analysis</span>

In software engineering, structured analysis (SA) and structured design (SD) are methods for analyzing business requirements and developing specifications for converting practices into computer programs, hardware configurations, and related manual procedures.

<span class="mw-page-title-main">Incremental computing</span> Software feature

Incremental computing, also known as incremental computation, is a software feature which, whenever a piece of data changes, attempts to save time by only recomputing those outputs which depend on the changed data. When incremental computing is successful, it can be significantly faster than computing new outputs naively. For example, a spreadsheet software package might use incremental computation in its recalculation feature, to update only those cells containing formulas which depend on the changed cells.

Node graph architecture is a software design structured around the notion of a node graph. Both the source code as well as the user interface is designed around the editing and composition of atomic functional units.

<span class="mw-page-title-main">Device driver synthesis and verification</span>

Device drivers are programs which allow software or higher-level computer programs to interact with a hardware device. These software components act as a link between the devices and the operating systems, communicating with each of these systems and executing commands. They provide an abstraction layer for the software above and also mediate the communication between the operating system kernel and the devices below.

For several years parallel hardware was only available for distributed computing but recently it is becoming available for the low end computers as well. Hence it has become inevitable for software programmers to start writing parallel applications. It is quite natural for programmers to think sequentially and hence they are less acquainted with writing multi-threaded or parallel processing applications. Parallel programming requires handling various issues such as synchronization and deadlock avoidance. Programmers require added expertise for writing such applications apart from their expertise in the application domain. Hence programmers prefer to write sequential code and most of the popular programming languages support it. This allows them to concentrate more on the application. Therefore, there is a need to convert such sequential applications to parallel applications with the help of automated tools. The need is also non-trivial because large amount of legacy code written over the past few decades needs to be reused and parallelized.

<span class="mw-page-title-main">RELAP5-3D</span>

RELAP5-3D is a simulation tool that allows users to model the coupled behavior of the reactor coolant system and the core for various operational transients and postulated accidents that might occur in a nuclear reactor. RELAP5-3D can be used for reactor safety analysis, reactor design, simulator training of operators, and as an educational tool by universities. RELAP5-3D was developed at Idaho National Laboratory to address the pressing need for reactor safety analysis and continues to be developed through the United States Department of Energy and the International RELAP5 Users Group (IRUG) with over $3 million invested annually. The code is distributed through INL's Technology Deployment Office and is licensed to numerous universities, governments, and corporations worldwide.

References

  1. ↑ 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
  2. ↑ "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.
  3. ↑ An analysis of ordnance software using the MALPAS tools, Hayman, K, Defence Sci. & Technol. Organ., Salisbury, SA. http://www.dsto.defence.gov.au/publications/scientific_record.php?record=9074
  4. ↑ 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
  5. ↑ "Computer based safety systems - technical guidance for assessing software aspects of digital computer based protection systems". Archived from the original on 2011-07-04.
  6. ↑ 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
  7. ↑ 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.{{cite web}}: CS1 maint: archived copy as title (link)
  8. ↑ https://www.newcivilengineer.com/latest/atkins-wins-hinkley-point-c-safety-contract-27-04-2020/
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.