15 Formal Verification

Question 1

What’s Verification?

Answer 1

Verify the correctness that is the absense of defects.
Specification must be given and must be formal.

Question 2

What’s Formal

Answer 2

3C: Completeness, Consistency, Clarity (unambiguous).
Descriptive or Operational Diagrams.

Question 3

Formal Methods

Answer 3

1. Constructing formal specification.
2. Performing formal verification.

Question 4

Hoarse Triple

Answer 4

Describes how the execution of a piece of code changes the state of the computation.

{P} C {Q}

P: Assertion/Precondition
C: Command
Q: Assertion/Post Condition

Question 5

Hoarse Logic Rules

Answer 5

Composition
Conditional
Consequence
While

Question 6

Horase Logic Axioms

Answer 6

Empty statement axiom: Skip statement does not change the state of the program.

Assignment Axiom: After the assignment, any predicate that we previously true for the right-hand side of the assignment now holds for the variables.

Question 7

Strongest Postconditions

Answer 7

A true condition that is the most useful/strict.

Question 8

Weakest Preconditions

Answer 8

A true pre-conditon that is the most useful/strict.

Question 9

Selective use of Formal Methods

Answer 9

Not an all or nothing approach.

Amount of formaility can vary
Need not build complete formal models.
Need not formally analyze every system property.
Need not apply FM in every phase of development.
Can choose what level of abstraction (amount of detail) to model.

Question 10

Light weight Formal Methods

Answer 10

Have become popular as a means of getting the technology transferred.

Two approaches:
1. Lightweight use of FMs: selectively apply FMs for partial modeling.
2. Lightweight FMs - new methods that allow unevaluated predicates.