Wednesday, 31 January 2018

Software Verification and Validation Topics - 2017

1a.The notion of Verification and Validation. Overview of typical verification and validation activities during software development. (L01a)

This includes verification of requirement specification
Modelling and verifying designs
Source code verification and unit testing

1b. Efficient verification of complex systems by symbolic model checking (L08a)
Included model checking with set operations
Representation of states with boolean function. Construction of characteristic function

2a. Basic formalism for modelling behavior: Kripke Structure. Labeled Transition System, Kripke Transition System, Finite Automata, Timed Automata

Kripke Structure: properties of state: labeling by AP
LTL: properties of transitions: labeling by actions
KTS: properties of both
FSA: states and transitions
TA: for modeling time-dependent behavior, labeling with clock-variables

2b. Formal relations for refinement checking: May Preorder and Must Preorder and their relationship with testing.

May Preorder: successful T1, may also be successful T2. preserved behavior
Must Preorder: successful T1, always successful T2. Non-determinism

3a. Verification of Software Requirement Specification: criteria and techniques

Complete, Consistent, Verifiable and Feasible
Techniques: Static Analysis(Manual Review and Tool Support)

3b. Verification of invariant properties by bounded model checking (BMC)
The state space is not handled all at once. Partial verification done by restricting the path of the state space.
Map the problem to a suitable SAT problem

4a. Verification of Software Architecture Design: criteria and techniques
Criteria includes: dependability, performance, maintainability, usability, testability
Techniques: ATAM(how does architecture satisfy quality objective and use of utility trees, Static Analysis and Quantitative Analysis

4b: Formalizing and checking requirements using LTL and HML

LTL: use of rule and symbolisms: linear and branching, AP, boolean operators and temporal operators
HML: LTS = (L, Act, ). Captures finite sequence of actions

5a. Verification of detailed design: criteria and techniques
Criteria include Local Characteristics of Completeness, Consistency, verifiability and feasiblility. Behavioral properties of safety and liveness
Techniques include Static and Dynamic Checking

5b. Model based test case generation by model checking and bounded model checking.
Bounded model checking restricts the path of the state space and maps the problem to a suitable SAT problem

6a. Role of development standards in the verification and validation of critical systems
Standards specifies safety functions and integrity levels.

6b. Software model checking with Counter-Example Guided Abstraction Refinement.
Creating a refined state space from the given concrete state space by hiding details.

7a. Verification of program source codes. Criteria and techniques
Checking for coding guidelines, software metrics, faulty patterns and run-time failures
Techniques include static analysis and code interpretation

7b.  Model-checking of timed dependent behavior - basic formalisms of timed-automata and timed temporal logic