Critical systems need to meet stringent dependability requirements, and we perform various verification and validation (V & V) processes that look for errors that affect the availability, safety, reliability and security of the system. During V & V, we attempt to show that the system meets the customer’s requirements, and in the process of doing this we will uncover many requirement specification, design and coding errors (and bugs) which will need to be repaired.
Critical systems need stringent testing for two reasons:
Cost of failure: The cost of system failure (life and property destruction, monetary and reputation loss) might be unacceptable, and it’s far cheaper to thoroughly test and analyse the system and remove all defects before it’s delivered.
Validation of dependability attributes: A record of how you validated the system might be important to get regulator and customer acceptance for your product. For a lot of critical system, the lack of regulator approval would mean your system cannot be used.
Due to these strict requirements, more than half the cost of developing a critical system goes into V & V. These are justified by the relatively huge costs if the system were to fail in a critical situation, such as the Ariane 5 explosion in 1996.
Another aspect of Dependability and Security Assurance is ensuring that proper software development processes are being followed. Good processes lead to good systems.
The outcome of these processes are a large body of evidence that justifies the developer’s claim of the system being dependable and safe for use.
Static analysis involves the analysis of the source representation of the software – be it a requirements document, design model or source code. It doesn’t involve actually executing the code and therefore can be done in any stage of the development lifecycle. They also have the added advantage of being safe from defects masking other defects, since you analyse the source code line by line.
The two common static analysis tools are manual analysis of designs and code (by a group of reviewers) and using design modelling tools to check for UML anomalies. For critical system, some extra analysis methods may be used, such as Formal verification, Model checking and Automated program analysis.
Formal verification involves producing a mathematical proof to show that the system conforms to its specification. Formal methods may be used at different stages of the V & V process, such as:
- A formal system specification maybe developed and mathematically analysed for inconsistencies. This can help discover specification errors and omissions.
- Mathematical arguments can be used to formally verify that the source code of the system is consistent with its formal specification. This can help discover programming and some design errors.
Since program code cannot directly be analysed formally, software tools are used to transform it into a format that can be analysed. The B method is probably the most widely used formal transformational method, used in train control systems and avionics software.
Although formal verification can help discover a lot of errors that would be impossible to detect otherwise (for example, by testing alone), there is no guarantee that a formal proof will ensure a reliable system in real world situations.
- The formal specification might not reflect the real requirements of system users, and since they are hard to understand by normal users, there’s no way to find errors and omissions directly.
- The proof may contain errors, since they’re large and complex (just like large and complex programs are more likely to contain errors).
- The proof might make incorrect assumptions about system usage, which might not be true in real life.
Formal verification is a costly and difficult process, involving a lot of mathematical knowledge. But, it can still be used to verify safety critical components, since it’s a very effective tool at discovering common specification problems that cause a majority of system failures.
Model checking is where a theorem prover is used to check the formal proof for inconsistencies. A formal model of the system is built, and expressed in a special model-checking system language, such as Promela for the SPIN system. A set of desirable system properties or states are identified and written in formal notation. The model checker then explores all possible execution paths through the system (state transitions) to see if the desirable properties hold. If a certain property doesn’t hold for a certain path, the model checker will output a counter-example showing where the property doesn’t hold true. Model checkers are very useful in checking concurrent systems, which are hard to test dynamically due to their sensitivity to time.
Issues with model checking include creating the system model, which is an expensive process if done manually. It’s best if it can automatically be generated from program source code. It is also an exhaustive process, which leads to a huge amount of computations needing to be performed – another reason it might be impractical for very large systems, since they would require a lot of computer time. But as algorithms improve, model checking is becoming a highly practical way to verify critical systems and embedded systems.
Automated static (program) analysis is the process of checking the source code for commonly known error-prone constructs and patterns (usually language-dependent), done using an automated static analyser. Programmers don’t need to learn specialised notation to use these tools, and it’s therefore easy to introduce and widely used in the development process.
Automated static analysers scan the source code of the program and detect potential errors. They can complement the error detection facilities offered by the compiler, and detect errors such as badly formed statements and problematic control flows. Although it cannot discover some classes of errors that are detected in manual reviews, it’s a very fast and cost-effective V & V method. The aim of static analysis is to highlight anomalies in the program code. These may not always be faults, and may have deliberately been introduced by the programmer. But they are things that could potentially go wrong during program execution and hence need to be reviewed by the programmer or reviewer. Static analysers have three levels of checking:
- Characteristic error checking – The analyser looks for common language dependent errors. Though relatively simple, this can be a very cost effective error detection method. (It was revealed in one research that 90% of C and C++ errors resulted from 10 common types of characteristic errors)
- User-defined error checking – Users of the analyser might define error patterns, and this is very useful for situations where ordering should be maintained. Organizations can add information regarding common bugs they have encountered over time to the system.
- Assertion checking – The most general and powerful method in static analysis. Developers include conditions (formal assertions) that must hold at different points of the program execution. A static analyser symbolically executes the code and shows any assertions that will not hold.
Static analysis is a very useful technique, but often produces a lot of ‘false positives’, where there are no errors but the analyser detects an anomaly. This number can be reduced by the use of assertions. The false positives have to be screened out before the code itself can be checked for errors.
Static analysis is also valuable for security testing, since attackers often target well-known vulnerabilities such as buffer overflows and unchecked inputs. Static analysers often detect these kinds of issues. Static analysers are also much better than security testers at detecting issues that only occur when the system is used in an unexpected way, and can incorporate detailed security expertise. You can claim that the program is valid for all possible program executions, and not just ones your testers have tested it for.
Static analysis is now routinely used by many organizations, such as Microsoft, in development of software such as device drivers and other software requiring security and reliability. Critical systems like nuclear and avionics systems are regularly statically analysed as part of V & V.
Research Paper: Software Model Checking Takes Off
Although the use of formal methods has been common in the design of safety- and security-critical systems, they have not achieved widespread use in software and systems engineering. But two new trends are helping change this:
- Tools such as MATLAB Simulink and Esterel Technologies SCADE Suite are helping make Model-Based Development (MBD) an accepted part of embedded systems design. MBD involves using domain-specific graphical modelling languages to execute and analyse models before the actual system is built. These languages and tools allow developers to create a model of the system, execute it, analyse it automatically and even output valid source code. The graphical models produced by these tools provide a formal (or nearly formal) specification, like that produced by formal analysis.
- The power of formal verification tools (particularly model checkers) are growing. They provide a “push-button” means of determining if a model meets its requirements, and examine all possible combinations of inputs and states – making the verification equal to exhaustive testing. If a properly isn’t true, the model will output a counterexample.
There are two types of model checkers. Explicit State Model Checkers construct and store a representation of each state visited, while Implicit State (Symbolic) Model Checkers use logical representations of sets of states such as Binary Decision Diagrams (BDD) to describe regions of the state space that satisfy the properties.