Verification of Discrete Systems - 06 Flashcards
What is the difference between validation and verification?
Validation focuses on whether the product being built is right for the customer’s requirements, whereas verification focuses on whether the product is being built correctly according to the product’s specifications.
What are the two different verification concepts and examples of each?
Informal methods:
* Code review or model inspection - Checking the specification by looking at the system
* Testing - Generation of input sequences for simulations or real tests
Formal methods:
* Automated theorem proving (using deduction)
* Model checking (using enumeration) - Exhaustive specification checking. Other than for testing, one can guarantee that all possible behaviors are considered.
What are the different types of tests setup?
SiL (Simulation in the loop) - Plant and controller simulated, HiL (Hardware in the loop) - Plant simulated and real controller and real test - Plant real and controller real.
What are different method of generation of test cases?
Manual generation: Ideally, test cases are manually generated by testers who are not developers.
Automatic generation: Randomized generation of inputs or generation of inputs, which maximizes a test metric (more difficult, but often more effective).
Most bugs are found early and rare faults are often undetected (formal methods), and various metrics measures the test progress.
What are the fundamentals for choosing metrics?
- From simple to complex metrics.
- A single metric is usually insufficient.
- There is no possibility of rigorously comparing testing metrics with each other.
- Test metrics make it possible to estimate the testing progress. However, there are no general guidelines on when to
finish testing based on the metric values. - Achieving a full coverage (100%) of a test metric does not imply the correctness of a system. (see, e.g., code
coverage). - Quality criteria:
– Overhead for computing the metric
– Effort to automatically generate inputs that improve the test metric
– Effort to integrate the test metric into the test environment.
What the most common metrics for FSA?
The most common metrics are:
* state coverage
* transition coverage
* path coverage (limited path length)
This can be applied analogously to Petri nets and statecharts since they can be transformed into finite state automata.
One often applies abstraction techniques to reduce the number of states to reduce the number of generated tests.
What are some advantages and disadvantages of testing?
Advantages:
* Not much preparation required
* No specially trained personnel required
* Good cost-benefit-ratio when only the most severe bugs have to be found
* Test metrics give an indication of the maturity of the system.
Disadvantages:
* Correctness cannot be guaranteed
* Subtle bugs are very hard to find
How can a theorem be proven?
By deduction or by enumeration.
What are the advantages and disadvantages of interactive theorem proving?
Advantages:
* Formal method → correctness can be proven
* Theorem provers can handle many problem classes (e.g., countable infinite number of states)
* No state explosion as in model checking
Disadvantages:
* Requires experts
* A theorem prover might not terminate even if a proof exists → no proof that the system is incorrect
* No counterexample as in model checking
What is the principle of Model Checking?
Principle of Model Checking:
1. SW/HW artifact → automated model extraction → Kripke structure
2. textual specification → manual translation → temporal logic
3. model checking → yes or no plus counterexample
What is the accepted LTL syntax formula?
p| ¬ϕ∣ϕ1 ∨ ϕ2∣X(ϕ)∣ϕ1Uϕ2.
What is the accepted CTL syntax formula?
p| ¬ϕ∣ϕ1 ∨ ϕ2∣E(ϕ)∣A(ϕ)
What are the major specifications in temporal logic and what are the formulations?
Reachability: CTL: EF(ϕ)
Safety: CTL: AG(¬ϕ), LTL: G(¬ϕ) (duality with reachability)
Liveness: CTL: AF(ϕ) or AG(ϕ 1=> AF(ϕ1)), LTL: F(ϕ) or G(ϕ 1=> F(ϕ1))
Fairness: CTL: AG(AF(ϕ)) (unconditional), LTL: GF(ϕ) (unconditional), strong fairness GF(ϕ1) => GF(ϕ2) and wak fairness, FG(ϕ1) => GF(ϕ2)
Name two popular model checkers.
SPIN and NuSMV
What are the advantages and disadvantages of model checking?
Advantages:
* Formal method - correctness can be guaranteed
* No proof required
* Fast computation (compared to other methods)
* Produces counterexamples
Disadvantage: State explosion.
