Formal V&V Techniques
Formal V&V techniques are based on formal mathematical proofs of correctness. If attainable, a formal proof of correctness is the most effective means of model V&V. Unfortunately, “if attainable” is the sticking point. Current formal proof of correctness techniques cannot even be applied to a reasonably complex simulation; however, formal techniques can serve as the foundation for other V&V techniques. The most commonly known techniques are briefly described below.
Induction, Inference, and Logical Deduction are simply acts of justifying conclusions on the basis of premises given. An argument is valid if the steps used to progress from the premises to the conclusion conform to established rules of inference. Inductive reasoning is based on invariant properties of a set of observations; assertions are invariants because their value is defined to be true. Given that the initial model assertion is correct, it stands to reason that if each path progressing from that assertion is correct and each path subsequently progressing from the previous assertion is correct, then the model must be correct if it terminates. Birta and Ozmizrak (1996) present a knowledge-based approach for M&S validation that uses a validation knowledge base containing rules of inference.
Inductive Assertions assess model correctness based on an approach that is very close to formal proof of model correctness. It is conducted in three steps.
- Input-to-output relations for all model variables are identified
- These relations are converted into assertion statements and are placed along the model execution paths so that an assertion statement lies at the beginning and end of each model execution path
- Verification is achieved by proving for each path that, if the assertion at the beginning of the path is true and all statements along the path are executed, then the assertion at the end of the path is true
If all paths plus model termination can be proved, by induction, the model is proved to be correct.
Lambda Calculus is a system that transforms the model into formal expressions by rewriting strings. The model itself can be considered a large string. Lambda calculus specifies rules for rewriting strings to transform the model into lambda calculus expressions. Using lambda calculus, the modeler can express the model formally to apply mathematical proof of correctness techniques to it.
Predicate Calculus provides rules for manipulating predicates. A predicate is a combination of simple relations, such as completed_jobs > steady_state_length. A predicate will be either true or false. The model can be defined in terms of predicates and manipulated using the rules of predicate calculus. Predicate calculus forms the basis of all formal specification languages.
Predicate Transformation verifies model correctness by formally defining the semantics of the model with a mapping that transforms model output states to all possible model input states. This representation is the basis from which model correctness is proved.
Formal Proof of Correctness expresses the model in a precise notation and then mathematically proves that the executed model terminates and satisfies the requirements with sufficient accuracy. Attaining proof of correctness in a realistic sense is not possible under the current state of the art. The advantage of realizing proof of correctness is so great, however, that, when the capability is realized, it will revolutionize V&V.
Informal V&V Techniques
Informal techniques are among the most commonly used. They are called informal because they rely heavily on human reasoning and subjectivity without stringent mathematical formalism. The informal label should not imply, however, a lack of structure or formal guidelines in their use. In fact, these techniques should be applied using well-structured approaches under formal guidelines. They can be very effective if employed properly.
The following techniques are discussed in the paragraphs below:
- Desk Checking / Self-inspection
- Face Validation
- Turing Test
- Inspection vs Walkthrough vs Review
2. Desk Checking / Self-inspection: Desk checking, or self-inspection, is an intense examination of a working product or document to ensure its correctness, completeness, consistency, and clarity. It is particularly useful during requirements verification, design verification, and code verification. Desk checking can involve a number of different tasks, such as those listed in the table below.
Typical Desk Checking Activities:
· Syntax review
· Cross-reference examination
· Convention violation assessment
· Detailed comparison to specifications
· Code reading
· Control flowgraph analysis
· Path sensitizing
To be effective, desk checking should be conducted carefully and thoroughly, preferably by someone not involved in the actual development of the product or document, because it is usually difficult to see one’s own errors.
3. Face Validation: The project team members, potential users of the model, and subject matter experts (SMEs) review simulation output (e.g., numerical results, animations, etc.) for reasonableness. They use their estimates and intuition to compare model and system behaviors subjectively under identical input conditions and judge whether the model and its results are reasonable.
Face validation is regularly cited in V&V efforts within the Department of Defense (DoD) M&S community. However, the term is commonly misused as a more general term and misapplied to other techniques involving visual reviews (e.g., inspection, desk check, review). Face validation is useful mostly as a preliminary approach to validation in the early stages of development. When a model is not mature or lacks a well-documented VV&A history, additional validation techniques may be required.
4. Inspection: Inspection is normally performed by a team that examines the product of a particular simulation development phase (e.g., M&S requirements definition, conceptual model development, M&S design). A team normally consists of four or five members, including a moderator or leader, a recorder, a reader (i.e., a representative of the Developer) who presents the material being inspected, the V&V Agent; and one or more appropriate subject matter experts (SMEs).
Normally, an inspection consists of five phases:
5. Follow up
5. Review: A review is intended to evaluate the simulation in light of development standards, guidelines, and specifications and to provide management, such as the User or M&S PM, with evidence that the simulation development process is being carried out according to the stated objectives. A review is similar to an inspection or walkthrough, except that the review team also includes management. As such, it is considered a higher-level technique than inspection or walkthrough.
A review team is generally comprised of management-level representatives of the User and M&S PM. Review agendas should focus less on technical issues and more on oversight than an inspection. The purpose is to evaluate the model or simulation relative to specifications and standards, recording defects and deficiencies. The V&V Agent should gather and distribute the documentation to all team members for examination before the review.
The V&V Agent may also prepare a checklist to help the team focus on the key points. The result of the review should be a document recording the events of the meeting, deficiencies identified, and review team recommendations. Appropriate actions should then be taken to correct any deficiencies and address all recommendations.
6. Turing Test: The Turing test is used to verify the accuracy of a simulation by focusing on differences between the system being simulated and the simulation of that system. System experts are presented with two blind sets of output data, one obtained from the model representing the system and one from the system, created under the same input conditions and are asked to differentiate between the two. If they cannot differentiate between the two, confidence in the model’s validity is increased. If they can differentiate between them, they are asked to describe the differences. Their responses provide valuable feedback regarding the accuracy and appropriateness of the system representation.
7. Walkthrough: The main thrust of the walkthrough is to detect and document faults; it is not a performance appraisal of the Developer. This point must be made to everyone involved so that full cooperation is achieved in discovering errors. A typical structured walkthrough team consists of:
- Coordinator, often the V&V Agent, who organizes, moderates, and follows up the walkthrough activities
- Presenter, usually the Developer
- Maintenance oracle, who focuses on long-term implications
- Standards bearer, who assesses adherence to standards
- Accreditation Agent, who reflects the needs and concerns of the UserAdditional reviewers such as the M&S PM and auditors
Inspection vs Walkthrough vs Review:
Inspections differ significantly from walkthroughs. An inspection is a five-step, formalized process. The inspection team uses the checklist approach for uncovering errors. A walkthrough is less formal, has fewer steps, and does not use a checklist to guide or a written report to document the team’s work. Although the inspection process takes much longer than a walkthrough, the extra time is justified because an inspection is extremely effective for detecting faults early in the development process when they are easiest and least costly to correct.
Inspections and walkthroughs concentrate on assessing correctness. Reviews seek to ascertain that tolerable levels of quality are being attained. The review team is more concerned with design deficiencies and deviations from the conceptual model and M&S requirements than it is with the intricate line-by-line details of the implementation. The focus of a review is not on discovering technical flaws but on ensuring that the design and development fully and accurately address the needs of the application. For this reason, the review process is effective early on during requirements verification and conceptual model validation.