Foundations of Softw... Complete Curriculum Fault-Tolerant Softw...

Software Test and Analysis (Software Verification and Validation)

Software Test and Analysis illustrated by means of real-world Applications

Lecture

"Vertrauen ist gut, Kontrolle ist besser!"

These lectures focus on techniques adopted in an industrial environment to identify the importance of software systems and components within a technical process that is to be automated. To do so, the impact of software failures on application-specific demands like safety, availability, and reliability will be investigated and classified. According to the degree of relevance identified, verification and validation techniques at increasing levels of rigor will be described and illustrated by real-world examples. These differ substantially in the phase of the software life-cycle to which they are applied.

Verification effort is invested to make sure that the software is developed correctly,i.e. providing a correct solution to a specified problem (making things right); this can be done only with respect to an unambiguous requirements specification. On the other hand, validation has to make sure that the problem has been accurately described, in order for the software developed to correctly reflect the requirements (making right things). This question must address the early and the latest phases of the software life-cycle by a rigorous analysis of the requirements as well as by extensive field testing.

Both the verification and the validation activities may include formal as well as informal approaches: formal techniques allow the application of logical inferential mechanisms for the purpose of mathematical proofs of correctness, whereas informal techniques are based on specific scenario-dependent behavioural observations to be extrapolated on more general input domains. A crucial challenge of today's software engineering community consists of determining relevant combinations of formal and informal correctness checks capable of implying a sufficient degree of trustworthiness dependent on the application-specific demands.


Contents
1. Introduction
2. Analysis at System Level
3. Risk Analysis
4. Requirements Validation
5. Verification by Control Flow Based Techniques
6. Verification by Data Flow Based Techniques
7. Test Adequacy Evaluation
8. Formal Methods
9. Combining Formal and Informal Approaches
Literature


Extended Contents

1. Introduction
Motivation & Aim, Definitions
Verification and Validation
Formal and Informal Techniques
Mistake, Fault, Error, Failure
Physical and Logical Failures
Hardware and Software Failures

2. Analysis at System Level
Characteristics of complex systems
Failure mode, effect and criticality analysis (FMECA)
      Aims and objectives
      Example: FMECA worksheet
Fault tree analysis (FTA)
      Approach and symbols, minimal cut sets
      Examples: notebook unavailability, pumping system
      Deriving minimal cut sets using algorithm by Quine / McCluskey
      Representation of complex boolean functions by ROBDDs
          Example: odd parity function, applications in safety engineering (incl. automatic test generation for integrated circuits)
      Determining minimal cut sets by ROBDDs (Rauzy's algorithm) with examples
Software Fault Tree Analysis (SFTA)
      Aim and advantages of SFTA, templates
      Examples: Satellite Control Program

3. Risk Analysis
Overall risk, partial risk, initiating events
Standard: "Messen-Steuern-Regeln, grundlegende Sicherheitsbetrachtungen für MSR-Schutzeinrichtungen " (DIN 19250)
      Risk parameters
      Examples: lifting platform, motorised windows and doors
Standard: "Functional Safety of Electrical/Electronic/Programmable Electronic Safety-related systems" (IEC 61508)
      Safety integrity levels
Motor Industry Software Reliability Association (MISRA) Guideline
      Integrity levels
      Example: specification of airbag

4. Requirements Validation
Causal logic
      Relations: direct cause, termination, sustainment, prevention
      Example: analysis of Warsaw airbus accident
Model checking
      CTL syntax and semantics
      Examples: mutual exclusion, cache consistency protocol, Elbtunnel project

5. Verification by Control Flow Based Techniques
Statement coverage
Branch coverage
    Examples: ZaehleZchn, WerteZiffernfolgeAus
Linear code sequence and jump (LCSAJ) test
Test effectiveness ratio (TER) hierarchy
Path testing
Structured testing, boundary interior path testing
    Examples: WerteZiffernfolgeAus, ZaehleZchn
Condition Coverage
      Complete vs. incomplete expression evaluation
      Simple condition coverage
          Example: complete evaluation vs. incomplete evaluation
      Condition/decision coverage
      Minimal multiple condition coverage
      Modified condition/decision coverage
      Multiple condition coverage
Subsumption hierarchy for control flow based testing techniques

6. Verification by Data Flow Based Techniques
Extension of control flow graphs
Data usage: defs, uses, c-uses, p-uses, imports, exports
    Examples: ZaehleZchn, MinMax
all defs coverage
all p-uses coverage
all c-uses coverage
all c-uses/some p-uses coverage
all p-uses/some c-uses coverage
all uses coverage
all du-paths coverage
Subsumption hierarchy for data flow based testing techniques
    Example: ZaehleZchn

7. Test Adequacy Evaluation
Mutation analysis
      Competent programmer hypothesis, coupling effect
      Mutation adequacy score
      Strong mutation testing
      Weak mutation testing
      Example: ZaehleZchn

8. Formal Methods
Proofs of correctness
      Theorem proving vs. model checking
      Partial and total correctness of programs
Axiomatic approaches
      Proving correctness of sequential programs by Hoare calculus
      Proving correctness of parallel disjoint programs
      Proving correctness of parallel programs with shared variables by Owicki/Gries method
            Atomicity, auxiliary variables, interference freedom, conjunction rule for parallel composition

9. Combining Formal and Informal Approaches
Complementarity of formal and informal approaches
Properties of testing criteria
      Reliable criterion
      Valid criterion
      Ideal criterion
Proof of correctness by ideal testing criterion
Uniform testing criterion
Proof of correctness by Goodenough/Gerhart
      Partitioning the input space into fault revealing subdomains
Proof of correctness by Geller
      Distributed correctness
      Test data assertion, generalisation assertion, synthesised assertion
      Examples: Manna's 91-function, leap year

Literature

Books
  • N. G. Leveson
    Safeware: System Safety and Computers - A Guide to Preventing Accidents and Losses Caused by Technology
    Addison-Wesley 1995

  • F. Ortmeier et al.
    Safety Analysis of the Height Control System for the Elbtunnel
    Proc. SAFECOMP 2002, LNCS 2434

  • Beatrice Berard
    Systems and Software Verification. Model-Checking Techniques and Tools
    Springer-Verlag Berlin Heidelberg

  • Peter Liggesmeyer
    Software-Qualität. Testen, Analysieren und Verifizieren von Software
    Spektrum, 2002

  • B.-U. Pagel and H.-W. Six
    Software Engineering, Band 1

  • Helmut Balzert
    Lehrbuch der Software-Technik
    Spektrum - Akademischer Verlag
    2001, Heidelberg, Band 2: Software Entwicklung

  • Krzysztof R. Apt, Ernst-Rudiger Olderog
    Verification of Sequential and Concurrent Programs
    Springer Verlag, 1997, 2nd edition

  • Articles
  • A. Rauzy
    New Algorithms for Fault Tree Analysis
    Reliability Engineering and System Safety 1993

  • J. D. Moffett, J. G. Hall, A. C. Coombes, J. A. McDermid
    A Model of a Causal Logic for Requirements Engineering
    Journal of Requirements Engineering, 1(1): 27-46. March 1996

  • A. Coombes, J. McDermid, J. Moffett
    Requirements Analysis and Safety: A Case Study (using GRASP)
    Proceedings of the 14th International Conference on Computer Safety, Reliability and Security (SAFECOMP '95), G. Rabe editor, Springer Verlag 1995

  • J. B. Goodenough and S. L. Gerhart
    Toward a Theory of Test Data Selection
    IEEE Transactions on Software Engineering, Vol SE-1, No 2, June 1975

  • M. Geller
    Test Data as an Aid in Proving Correctness
    Communications of the ACM, May 1978, Volume 21, Number 5

  • top