1a.The notion of Verification and Validation. Overview of typical verification and validation activities during software development. (L01a)<\/b><\/p>\n
This includes verification of requirement specification
\nModelling and verifying designs
\nSource code verification and unit testing<\/p>\n
<\/p>\n
1b. Efficient verification of complex systems by symbolic model checking (L08a)<\/b>
\nIncluded model checking with set operations
\nRepresentation of states with boolean function. Construction of characteristic function<\/p>\n
\n<\/b>2a. Basic formalism for modelling behavior: Kripke Structure. Labeled Transition System, Kripke Transition System, Finite Automata, Timed Automata<\/b><\/p>\n
Kripke Structure<\/i>: properties of state: labeling by AP
\nLTL<\/i>: properties of transitions: labeling by actions
\nKTS<\/i>: properties of both
\nFSA<\/i>: states and transitions
\nTA<\/i>: for modeling time-dependent behavior, labeling with clock-variables<\/p>\n
\n<\/b>2b. Formal relations for refinement checking: May Preorder and Must Preorder and their relationship with testing.<\/b><\/p>\n
May Preorder: successful T1, may also be successful T2. preserved behavior
\nMust Preorder: successful T1, always successful T2. Non-determinism<\/p>\n
<\/p>\n
3a. Verification of Software Requirement Specification: criteria and techniques<\/b><\/p>\n
Complete, Consistent, Verifiable and Feasible
\nTechniques: Static Analysis(Manual Review and Tool Support)<\/p>\n
<\/p>\n
3b. Verification of invariant properties by bounded model checking (BMC)<\/b>
\nThe state space is not handled all at once. Partial verification done by restricting the path of the state space.
\nMap the problem to a suitable SAT problem<\/p>\n
<\/p>\n
4a. Verification of Software Architecture Design: criteria and techniques<\/b>
\nCriteria includes: dependability, performance, maintainability, usability, testability
\nTechniques: ATAM(how does architecture satisfy quality objective and use of utility trees, Static Analysis and Quantitative Analysis<\/p>\n
<\/p>\n
4b: Formalizing and checking requirements using LTL and HML<\/b><\/p>\n
LTL: use of rule and symbolisms: linear and branching, AP, boolean operators and temporal operators <\/p>\n 5a. Verification of detailed design: criteria and techniques<\/b> <\/p>\n 5b. Model based test case generation by model checking and bounded model checking.<\/b> <\/p>\n 6a. Role of development standards in the verification and validation of critical systems<\/b> <\/p>\n 6b. Software model checking with Counter-Example Guided Abstraction Refinement.<\/b> <\/p>\n 7a. Verification of program source codes. Criteria and techniques<\/b> 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 … <\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"_mi_skip_tracking":false,"_monsterinsights_sitenote_active":false,"_monsterinsights_sitenote_note":"","_monsterinsights_sitenote_category":0},"categories":[359],"tags":[545],"_links":{"self":[{"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/posts\/169"}],"collection":[{"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/comments?post=169"}],"version-history":[{"count":2,"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/posts\/169\/revisions"}],"predecessor-version":[{"id":770,"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/posts\/169\/revisions\/770"}],"wp:attachment":[{"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/media?parent=169"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/categories?post=169"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/kindsonthegenius.com\/blog\/wp-json\/wp\/v2\/tags?post=169"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}
\nHML: LTS = (L, Act, \u2192<\/span>). Captures finite sequence of actions<\/p>\n
\nCriteria include Local Characteristics of Completeness, Consistency, verifiability and feasiblility. Behavioral properties of safety and liveness
\nTechniques include Static and Dynamic Checking<\/p>\n
\nBounded model checking restricts the path of the state space and maps the problem to a suitable SAT problem<\/p>\n
\nStandards specifies safety functions and integrity levels.<\/p>\n
\nCreating a refined state space from the given concrete state space by hiding details.<\/p>\n
\nChecking for coding guidelines, software metrics, faulty patterns and run-time failures
\nTechniques include static analysis and code interpretation<\/p>\n","protected":false},"excerpt":{"rendered":"