Validation, Verification and Formal Methods

Question 1

Validation of critical systems (recap)

Answer 1

• Critical systems involve additional validation processes and analysis than non-critical systems:
  
  • The costs and consequences
    of failure are high so it is
    cheaper to find and remove
    faults than to pay for system
    failure;
  • You may have to make a
    formal case to customers or to
    a regulator that the system
    meets its dependability
    requirements.
  • This dependability case may
    require specific Verification &
    Validation activities to be
    carried out.

Question 2

How much does validation cost usually?

Answer 2

• Normally, Validation & Verification costs take up more than 50% of the total system development costs.
• The outcome of the validation process is a tangible body of evidence that demonstrates the level of dependability of a software system.

Note: Because of the additional activities involved, the validation costs for critical systems are usually significantly higher than for non-critical systems.

Question 3

What is meant by Static Analysis (Technique)?

Answer 3

Meaning: Static analysis techniques are system verification techniques that do not involve executing a program.

Note: They work on a source representation of the software, i.e., either a model or the program code itself.

Examples of Static Analysis: Code Inspections and Reviews.

Other examples of Validation and Verification techniques include: Formal verification including model checking and automated program analysis.

Question 4

Note on Verification and formal methods.

Answer 4

Formal methods can be used when a mathematical specification of the system is produced.

Note: The mathematical specification is based on well-understood mathematical theories such as formal logic and set theory.

Note: Used in the development of some critical systems.

Question 5

What are Formal Methods?

Answer 5

Meaning: Formal methods are system design techniques that use rigorously specified
mathematical models to build software and hardware systems.

Note: Include verification techniques that may be used at different stages in the
development process, for instance:

• A formal specification may be developed and mathematically analysed for consistency.
• This helps discover specification errors and omissions.
• Formal arguments that a program conforms to its mathematical specification may be developed. This is effective in discovering programming and design errors.

Question 6

Notes on Formal Methods

Answer 6

As always this is not a panacea (solution):

• “It is very important to note that formal verification does not obviate (remove) the need for testing”.
• “Formal verification cannot fix bad assumptions in the design, but it can help identify errors in reasoning which would otherwise be left unverified.”
• “In several cases, engineers have reported finding flaws in systems once they reviewed their designs formally.”

Question 7

What are the advantages of Format Methods?

Answer 7

1. Producing a mathematical specification requires a detailed analysis of the requirements and this is likely to uncover errors (aids with error detected in requirements).
2. They can detect implementation errors before testing when the program is analysed alongside the specification.

Question 8

What are the Disadvantages of Formal Methods?

Answer 8

1. They require the use of specialised notations that cannot be understood by domain experts.
2. Very expensive to develop a specification and even more expensive to show that a program meets that specification.
3. Mathematical Proofs may contain errors.
4. It may be possible to reach the same level of confidence in a program more cheaply using other V & V techniques. (Might be more cheaper to get the same level of confidence using other cheaper V & V techniques).

Question 9

What is meant by model checking?

Answer 9

Meaning: A technique that verifies whether a system’s finite-state model meets a given specification.

Note: The model checker explores all possible paths through the model and checks
that a user-specified property is valid for each path.

Note: Model checking is particularly valuable for verifying concurrent systems, which are hard to test.

Note: Although model checking is computationally very expensive, it is now practical to use it in the verification of small to medium sized critical systems.

Question 10

What is meant by Static Analysis

Answer 10

Meaning: A testing method that examines/analyses the code without executing the program.

Note: Static analysers are software tools for source text processing.

Note: They parse the program text and try to discover potential error conditions and bring these to the attention of the V & V team.

Note: They are very effective as an aid to program inspections.

Disadvantage: Inspections can catch errors of understanding that tools can’t.

Question 11

Name and Describe all levels of static analysis?

Answer 11

Characteristic error checking:
* Check for code patterns that
are characteristic of errors
made by programmers using a
particular language.

User-defined error checking:
* Users of a programming
language dene error patterns,
thus extending the types of
error that can be detected. This
allows specific rules that apply
to a program to be checked.

Assertion checking:
* Developers include formal
assertions in their program and
relationships that must hold.
The static analyser symbolically
executes the code and
highlights potential problems.

Question 12

Name all automated static analysis checks. (5 fault classes, 15 checks)

Answer 12

Data Faults:
* Variables used before
initialization
* Variables declared but never
used
* Variables assigned twice but
never used between
assignments.
* Possible array bound violations
* Undeclared variables

Control Faults:
* Unreachable code
* Unconditional branches into
loops

Input/Output Faults:
* Variables output twice with no
intervening assignment.

Interface Faults:
* Parameter-type mismatches
* Parameter number
mismatches
* Non-usage of the results of
functions
* Uncalled functions and
procedures

Storage Management Faults:
* Unassigned Pointers
* Pointer Arithmetic
* Memory Leaks

Question 13

Where can Static Analysis be used? (2 cases)

Answer 13

1. Valuable for languages such as C, JS is used which has weak
   typing and hence many errors are undetected by the compiler.
2. Valuable for security checking - the static analyser can discover
   areas of vulnerability such as buffer overflows or unchecked inputs.

Key Note: Static analysis is now routinely used in the development of many safety and
security critical systems.

Question 14

What is meant by Statistical Testing?

Answer 14

Meaning: A method for testing software for reliability rather than fault detection.

Note: Measuring the number of errors allows the reliability of the software to be predicted. Note that, for statistical reasons, more errors than are allowed for in the reliability specification must be induced.

Note: An acceptable level of reliability should be specified and the software tested and amended until that level of reliability is reached.

Question 15

Notes on creating operation profile from real data

Answer 15

Note: A set of test data whose frequency matches the actual frequency of these inputs from ‘normal’ usage of the system. A close match with actual usage is necessary otherwise the measured reliability will not be reflected in the actual usage of the system.

Note: It can be generated from real data collected from an existing system or (more often) depends on assumptions made about the pattern of usage of a system.

Note: It can change as you learn how the system really works.

Question 16

Explain various reliability validation activities, step by step?
(4 steps)

Answer 16

1. Establish the operational prole for the system.
2. Construct test data reflecting the operational profile.
3. Test the system and observe the number of failures and the times of these failures.
4. Compute the reliability after a statistically significant number of failures have been observed.

Question 17

What are some of the problems faced when measuring reliability?

Answer 17

1. Operational profile uncertainty
   * The operational prole may not
   be an accurate reflection of
   the real use of the system.
2. High costs of test data
   generation.
3. Statistical uncertainty
   
   • You need a statistically
     significant number of failures
     to compute the reliability but
     highly reliable systems will
     rarely fail.
4. Recognising Failure
   
   • It is not always obvious when
     a failure has occurred as
     there may be conflicting
     interpretations of a
     specification.

Question 18

Notes on Examples of industries using formal methods

Answer 18

Complex computer-driven systems: fly-by-wire airplanes, medical systems, automated stock trading, networked industrial automation systems.

Note: Significant progress in formal methods allows these systems to be modelled in a mathematically precise way.

Note: Model checking: automated technique to prove that a model satisfies formally specified requirements.

Note: Crucial for establishing correctness.

Question 19

Last Few Notes

Answer 19

There is a huge variety in LTS-based models that can be used in verification and simulation.

Extensions include time, cost and probabilities in different ways.

Can be used for addressing dependability attributes

Analyse the behaviour of complex systems and understand emergent behaviour

Formal methods often do not scale well and cannot be as expressive as possibly desired.

Question 20

Summary of Topic (Validation, Verification and Formal Methods)

Answer 20

Static analysis is an approach to V & V that examines the source code (or other representation) of a system, looking for errors and anomalies. It allows all parts of a program to be checked, not just those parts that are exercised by system tests, but has limitations.

Model checking can be seen as a formal approach to static analysis that exhaustively checks all states in a system for potential errors.

Statistical testing is used to estimate software reliability. It relies on testing the system with a test data set that reflects the operational prole of the software.

Formal methods are key for many critical system domains.