[SoftwareV&V] 02. Framework

[원문링크]

https://adorable-aspen-d23.notion.site/SoftwareV-V_02_Framework-5c5176c41824429bbd25fe3f50eb6b37

SoftwareV&V_02_Framework

[2021 - 1학기 수강한 Software V&V 강의 정리본입니다.]

(Software Verification & Validation)

 

Framework for STA

Learning Objectives

• Test and analysis 의 차원과 tradeoff 살펴보기
• verification, validation 구분하기
• Test and analysis 의 장,단점 이해하기

1. Validation VS Verification

2. V-Model

3. 한계점 (Undeciability of Correctness Properties)

: 아무리 testing을 충분히 해도, 모든 오류를 잡을 수 없고 spec에 맞는지 알 수 없다.

• Halting problem: 어떤 프로그램과 입력을 받았을 때, 그 프로그램을 실행했을 때 유한한 단계 후에 끝날지 혹은 영원히 끝나지 않을지를 판별할 수 있는 일반적인 방법이 있을까를 다루는 문제
• ex) 드론이 날아가는데 '가끔' 떨어지는 상황을 testing으로 만들어 낼 수 없음
• : 에러가 나는 상황을 재현해 낼 수 없는 상황

4. Verification Trade-off Dimensions (섞어서 사용하자!) #26

1. Optimistic inaccuracy→ testing을 아무리 해도 error를 다 찾지 못한다.
2. : testing 후 true가 나오면 (spec에 문제가 있을 수 있겠지만) correct하다고 생각한다.
3. Pessimistic inaccuracy

: 코드를 실행시키지 않고 내부적으로 검사함. (Automated program Analysis = Static code Analysis)

→ False Alarm이 존재해서 프로그램을 보장할 수 없다.

1. Simplified Properties

: 모델을 만들어서 check한다.

→ 모델 만드는 것이 어려움

5. Pessimistic, Optimistic과 연관된 용어들 (시험)

1. Safe(safe analysis는 오직 옳은 프로그램만 허락하기 때문에 optimistic inaccuracy는 없다.)(다른 프로그램 분석에서는, safety가 최종 목적이다.)(예를 들어 '프로그램 최적화'와 관련된 safe 분석은 이 최적화의 결과가 정확할 때만 최적화를 허용하는 것이다.
2. For example, a safe analysis related to a program optimization is one that allows that optimization only when the result of the optimization will be correct.
3. In other kinds of program analysis, safety is related to the goal of the analysis.
4. : A safe analysis has no optimistic inaccuracy, that is it accepts only correct programs.
5. Sound

: An analysis of a program P with respect to a formula F is sound, if the analysis returns True only when the program actually does satisfy the formula

(Sound하다 : 프로그램이 실제로 formula를 만족시킬 때만 분석은 True를 반환한다.)

만족 안 시키면 → 무조건 False

Soundness is a term to describe evaluation of formulas.

• Soundness : 공식을 평가하는데 쓰인다.

If satisfaction of a formula F is taken as and indication of correctness, then a sound analysis is the same as a safe or conservative analysis(pessimistic)

• 공식F를 만족하는 것을 correctness의 표시로 삼는다면, Sound analysis는 safe 혹은 conservative analysis와 같다.

If the sense of F is reversed ( if the truth of F indicates a fault rather than correctness) then a sound analysis is not necessarily conservative. In that case it is allowed optimistic inaccuracy but must not have pessimistic inaccuracy. (However, that use of the term 'sound' has not always been consistent in the software engineering literature. Some writers use the term 'unsound' as we use the term optimistic.)

• 공식 F를 만족하는 것을 falut의 표시로 삼는다면, Sound analysis가 반드시 conservative analysis한 것은 아니다.
• 이 경우 optimistic inaccuracy를 허락하지만 pessimistic을 반드시 가지고 있지 않다.
• Sound = Pessimistic // Unsound = Optimistic 으로 쓰기도 한다.
  1. Complete
• Soundness와 비슷하게 공식을 평가할 때 쓰인다.

An analysis of a program P with respect to a formula F is 'complete' if the analysis always returns True when the program actually does satisfy the formula.

• Complete하다 : 프로그램이 실제로 공식을 만족할 때 항상 True를 반환한다.

만족 안 시키면 → 모름

If satisfaction of a formula F is taken as an indication of correctness, then a complete analysis is one that admits only optimistic inaccuracy.

• 공식 F를 만족하는 것을 correctness의 표시로 삼는다면, Complete analysis는 Optimistic inaccuracy만을 인정한다.

An analysis

sound but imcomplete → conservative analysis. (pessimistic)

unsound but complete → optimistic inaccuracy.

 

Summary

• 대부분의 property들은 undecidable하다. > 사람이 개입해야 한다.
• program quality를 assess하는 것은 두 가지로 나눌 수 있다. Validation / Verfication
• 하나의 technique로만 V&V가 이루어지지 않는다.

---

<aside> 💡 https://ix.cs.uoregon.edu/~michal/book/SampleChapters/PezzeYoung-Ch02-Framework.pdf 해석

</aside>

In a few domains, logical correctness arguments may even be cost-effective for a few isolated, critical components (e.g., a safety interlock in a medical device). In general, though, one cannot produce a complete logical “proof” for the full specification of practical programs in full detail.

• 수학적으로 나타낼 수 있을 것 같지만 critical 한 것 들과 같은 것들은 불가능하다.

In particular, logical contradictions ensue from assuming that there is some program P that can, for some arbitrary halting problem program Q and input I, determine whether Q eventually halts. To avoid those logical contradictions, we must conclude that no such program for solving the “halting problem” can possibly exist.

• Halting problem은 해결할 수 없다.

Program testing is a verification technique and is as vulnerable to undecidability as other techniques. Exhaustive testing, that is, executing and checking every possible behavior of a program, would be a “proof by cases,” which is a perfectly legitimate way to construct a logical proof. How long would this take? If we ignore implementation details such as the size of the memory holding a program and its data, the answer is “forever.” That is, for most programs, exhaustive testing cannot be completed in any finite amount of time.

• Testing에서 Undecidability를 해결하기 위해 Exhaustive testing을 사용할 수 없는 이유
• Forever 하기 때문

It may be pessimistic, meaning that it is not guaranteed to accept a program even if the program does possess the property being analyzed,

• 분석된 property를 보유하고 있다고 하더라도, 프로그램을 보장할 수 없다.

or it can be optimistic if it may accept some programs that do not possess the property (i.e., it may not detect all violations)

• property를 소유하지 않는 프로그램을 수용할 수 있는 경우 ( 모든 violation들을 찾지 않는다)
• → false alarm

Testing is the classic optimistic technique, because no finite number of tests can guarantee correctness.

• Testing은 무한한 모든 경우를 할 수 없으니 optimisitc이다

Many automated program analysis techniques for properties of program behaviors are pessimistic with respect to the properties they are designed to verify.

• 자동 프로그램 analysis는 pessimistic하다.

A software verification technique that errs only in the pessimistic direction is called a conservative analysis. It might seem that a conservative analysis would always be preferable to one that could accept a faulty program

• pessimistic = conservative analysis
• pessimistic 분석이 fault가 있는 프로그램을 받아들일 수 있는 분석보다 바람직하다.

However, a conservative analysis will often produce a very large number of spurious error reports, in addition to a few accurate reports.

• conservative → 쓸데없는 error가 자주 나옴. (False Alarm)