**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**