런타임 확인

런타임 검증은 실행 중인 시스템에서 정보를 추출하여 이를 사용하여 특정 속성을 만족하거나 위반하는 관찰된 행동을 탐지하고 이에 반응하는 컴퓨팅 시스템 분석 및 실행 접근 방식이다.^[1]데이터레이스나 교착상태의 자유와 같은 일부 매우 특별한 특성은 일반적으로 모든 시스템에 의해 충족되기를 원하며 알고리즘적으로 가장 잘 구현될 수 있다.다른 속성들은 형식적인 사양으로 보다 편리하게 포착할 수 있다.런타임 검증 규격은 일반적으로 유한 상태 기계, 정규식, 문맥 없는 패턴, 선형 시간 로직 등과 같은 추적 술어로 표현된다.이것은 일반 시험보다 덜 임시적인 접근을 허용한다.그러나 실행 시스템을 모니터링하기 위한 모든 메커니즘은 시험이나 참조 구현에^{[citation needed]} 대한 검증을 포함하여 런타임 검증으로 간주된다.형식 요건 사양이 제공되면, 그것들로부터 모니터를 합성하여 계측을 통해 시스템 내에 주입한다.런타임 검증은 보안 또는 안전 정책 모니터링, 디버깅, 테스트, 검증, 검증, 프로파일링, 결함 보호, 행동 수정(예: 복구) 등과 같은 여러 목적으로 사용할 수 있다.런타임 검증은 1개 또는 몇 개의 실행 추적만을 분석하여 실제 시스템과 직접 작용함으로써 모델 확인, 정리 증명과 같은 전통적인 형식 검증 기법의 복잡성을 방지하므로 비교적 잘 스케일업하여 분석 결과에 대한 신뢰도를 높인다(테디오를 피하기 때문에).더 적은 커버리지 비용으로 시스템을 공식적으로 모델링하는 오류 발생 가능성이 있는 단계더욱이, 반사 기능을 통해 런타임 검증은 대상 시스템의 필수적인 부분으로 만들어질 수 있으며, 배치 중에 그것의 실행을 감시하고 지도할 수 있다.

역사와 맥락

시스템이나 프로그램을 실행하지 않고 공식적으로 또는 비공식적으로 지정된 속성을 확인하는 것은 오래된 주제(고지한 예로는 소프트웨어의 동적 타이핑 또는 하드웨어의 페일 세이프 장치 또는 감시 타이머)로, 정확한 루트를 식별하기 어렵다.용어 런타임 검증은 형식 검증과 시험 사이의 경계에서 문제를 해결하기 위한 2001년 워크숍의^[2] 이름으로 공식적으로 도입되었다.대형 코드 베이스의 경우 테스트 케이스를 수동으로 작성하는 데 시간이 많이 소요되는 것으로 나타났다.또 개발 과정에서 모든 오류를 검출할 수 있는 것은 아니다.자동 검증에 대한 초기 기여는 우주선, 탐사선 및 항전 기술에서의 높은 안전 기준을 보관하기 위해 클라우스 해블룬드와 그리고레 로수에 의해 NASA 에임스 연구 센터에서 이루어졌다.^[3]시간적 논리로 사양을 검증하고 단일 실행경로를 분석해 자바 프로그램의 레이스 상태와 교착상태를 탐지할 수 있는 도구를 제안했다.

현재 런타임 검증 기법에는 런타임 모니터링, 런타임 확인, 런타임 반사, 런타임 분석, 동적 분석, 런타임/동적 심볼 분석, 추적 분석, 로그 파일 분석 등 다양한 대체 이름이 제시되는 경우가 많은데, 모두 d에 적용된 동일한 상위 개념의 인스턴스를 지칭한다.다른 지역 또는 다른 지역사회의 학자들에 의해.런타임 검증은 전개 전에 사용할 경우 시험(특히 모델 기반 시험)과 전개 중에 사용할 경우 내결함성 시스템과 같이 잘 확립된 다른 영역과 밀접하게 관련되어 있다.

런타임 검증의 넓은 영역 내에서 다음과 같은 몇 가지 범주를 구별할 수 있다.

• 원자성과 같은 대부분 동시성 관련 속성의 고정 집합을 대상으로 하는 "무중단" 모니터링.이 지역의 선구적인 작업은 세비지 외 지우개 알고리즘에^[4] 의한 것이다.
• 시간적 논리 규격에 관한 모니터링; 이 방향의 초기 기여는 리, 칸난과 그들의 협력자들,^[5][6] 그리고 하블룬드와 로수에 의해 이루어졌다.^[7][8]

기본 접근 방식

런타임 검증 방법의 넓은 분야는 다음과 같은 3차원으로 분류할 수 있다.^[9]

• 시스템은 실행 자체(온라인) 또는 실행 후 로그 분석(오프라인)의 형태로 모니터링할 수 있다.
• 검증 코드는 시스템에 통합되거나(양면 지향 프로그래밍에서와 같이) 외부 실체로 제공된다.
• 모니터는 원하는 규격의 위반 또는 유효성 검사를 보고할 수 있다.

그럼에도 불구하고 런타임 검증의 기본 프로세스는 여전히 유사하다.^[9]

1. 모니터는 어떤 공식적인 규격에서 생성된다.이 프로세스는 일반적으로 속성이 지정된 공식 언어에 대해 동등한 자동화가 있는 경우 자동으로 수행될 수 있다.정규식을 변환하기 위해 유한 상태 기계를 사용할 수 있다; 선형 시간 논리의 속성은 Büchi 자동화로 변환될 수 있다(Büchi 자동화에 대한 선형 시간 논리 참조).
2. 시스템은 실행 상태에 관한 이벤트를 모니터로 전송하도록 계측된다.
3. 시스템이 실행되어 모니터에 의해 검증된다.
4. 모니터는 수신된 이벤트 추적을 확인하고 규격의 충족 여부를 판정한다.또한 모니터는 시스템에 피드백을 보내 거짓 행동을 시정할 수 있도록 한다.오프라인 모니터링을 사용할 때 원인 시스템은 나중에 확인되므로 어떠한 피드백도 받을 수 없다.

예

아래 예에서는 이 작성 시점(2011년 4월)까지 여러 런타임 검증 그룹에 의해 검토된 몇 가지 간단한 속성에 대해 논의한다.그것들을 더 흥미롭게 하기 위해, 아래의 각 속성은 다른 규격 형식주의를 사용하며 모두 파라메트릭이다.파라메트릭 속성은 파라메트릭 이벤트로 형성된 트레이스에 대한 속성이며, 이는 데이터를 파라미터에 바인딩하는 이벤트다.여기서 매개 변수 속성은 $\forall {\displaystyle \mathrm{}}$ ${\displaystyle p}$ a ${\displaystyle a}$ a m ${\displaystyle e}$ t ${\displaystyle e}$ ${\displaystyle r}$ ${\displaystyle s}$ :${\displaystyle \phi }${\$displaystyle \forall parameters:\varphi }$ 형식이며$,$ 여기서 $\phi {\displaystyle }$ ${\displaystyle \varphi }$은 일반(제시되지 않은) 매개 변수 이벤트를 참조하는 적절한 형식주의에서 지정이다.$이러한{\displaystyle }$ 파라메트릭 속성의 직관은 ▼ ${\displaystyle \varphi }$에 의해 표현된 속성이 관측된 트레이스에서 (파라메트릭 이벤트를 통해) 만나는 모든 파라미터 인스턴스에 대해 유지되어야 한다는$$ 것이다.매개변수에 대한 지원이 분명히 필요하지만, 다음 예시 중 어느 것도 특정 런타임 검증 시스템에 특정되지 않는다.다음의 예에서 자바 구문을 가정하면, 따라서 "=="는 논리적 평등인 반면, "="는 할당이다.일부 방법(예:update()안전하지 않은 EnumExample)에는 명확성을 위해 사용되는 Java API의 일부가 아닌 더미 방법이 있다.

HasNext

Java Iterator 인터페이스는hasNext()방법이 호명되어 진실로 되돌아가다next()메소드를 호출한다.이 문제가 발생하지 않으면 사용자가 컬렉션의 "끝에서 꺼짐"을 반복할 가능성이 매우 높다.오른쪽 그림은 런타임 검증으로 이 속성을 확인하고 시행하기 위한 가능한 모니터를 정의하는 유한 상태 시스템을 보여준다.알 수 없는 상태에서는 항상 전화를 거는 것이 오류다.next()그러한 수술은 안전하지 않을 수 있기 때문에 방법.만약hasNext()부름을 받고 돌아온다.true, 전화하는 것은 안전하다.next()그래서 모니터는 더 많은 상태로 들어간다.그러나 만약, 만약hasNext()방법의 반환false, 더 이상 요소가 없고, 모니터는 없음 상태로 들어간다.더 많은 주와 더 없는 주에서는hasNext()방법은 새로운 정보를 제공하지 않는다.전화하는 것은 안전하다.next()메소드는 더 많은 상태에서 생성되지만 더 많은 요소가 존재하면 알 수 없게 되므로 모니터는 초기 알 수 없는 상태를 다시 입력한다.마지막으로, 전화하기next()없음 상태의 메서드는 오류 상태를 입력하게 된다.다음은 파라메트릭 과거 시간 선형 시간 논리를 사용하여 이 속성을 나타낸 것이다.

${\displaystyle \forall ~{\text{Iterator}~i\quad i.{\text{next}}()(~)~\오른쪽 화살표~\odot(i).{\text{hasNext}}(==true)}$

이 공식에 따르면 모든 전화는next()방법은 에 대한 호출을 즉시 선행해야 한다.hasNext()진실로 돌아오는 방법여기서 속성은 Iterator의 파라메트릭임i개념적으로, 이것은 런타임 검증 시스템이 파라메트릭 모니터를 이런 식으로 구현할 필요는 없지만, 시험 프로그램에서 가능한 각 Iterator에 대한 모니터의 복사본이 한 개 있을 것이라는 것을 의미한다.이 속성에 대한 모니터는 공식이 위반될 때(유한 상태 기계가 오류 상태로 들어갈 때 동등하게) 핸들러를 트리거하도록 설정되며, 다음 중 하나에 해당하는 경우에 발생한다.next()첫 번째 호출 없이 호출됨hasNext(), 또는 언제hasNext()전에 불려지다next(), 그러나 반환됨false.

안전하지 않은 에넘

자바의 벡터 클래스는 그 요소들을 반복하기 위한 두 가지 수단을 가지고 있다.하나는 앞의 예에서 보듯이 Iterator 인터페이스를 사용하거나 Enumeration 인터페이스를 사용할 수 있다.Iterator 인터페이스에 대한 제거 방법의 추가 이외에도 Iterator는 "fail fast"인 반면 Enumeration은 그렇지 않다는 것이 주된 차이점이다.즉, Iterator, ConcurrentModification을 사용하여 Vector를 반복할 때 Vector를 수정하는 경우(Iterator 제거 방법을 사용하지 않는 경우)예외는 던져진다.그러나 Enumeration을 사용할 때 언급된 바와 같이 이것은 사례가 아니다.이는 Enumeration의 관점에서 벡터가 일관되지 않은 상태로 방치되기 때문에 프로그램에서 결정적이지 않은 결과를 초래할 수 있다.Enumeration 인터페이스를 여전히 사용하는 레거시 프로그램의 경우, 기본 Vector를 수정할 때 Enumerations를 사용하지 않도록 강제할 수 있다.다음과 같은 파라메트릭 정규 패턴을 사용하여 이러한 동작을 시행할 수 있다.

∀ 벡터 v, 열거 e: (e = v.element() (.nextElement()^* v.update() e.nextElement() e.e.nextElement()

이 패턴은 Enumeration과 Vector의 파라메트릭이다.직관적으로 그리고 위의 런타임 검증 시스템은 이러한 방식으로 파라메트릭 모니터를 구현할 필요가 없으므로, 이 속성에 대한 파라메트릭 모니터를 가능한 각 벡터 및 열거 쌍에 대해 비모수 모니터 인스턴스를 생성하고 추적하는 것으로 생각할 수 있다.일부 이벤트는 다음과 같이 동시에 여러 모니터와 관련이 있을 수 있다.v.update()그래서 런타임 검증 시스템은 그것들을 모든 관심 있는 모니터에 (개념적으로) 발송해야 한다.여기에는 프로그램의 나쁜 행동을 명시하도록 속성이 명시되어 있다.이 속성은 패턴의 일치 여부를 모니터링해야 한다.오른쪽 그림은 이 패턴과 일치하는 자바코드를 나타내므로 속성을 위반한다.Vector, v는 Enumeration, e가 생성된 후 업데이트되며, 그 다음 e가 사용된다.

세이프락

앞의 두 예는 유한 상태 속성을 보여주지만, 런타임 검증에 사용되는 속성은 훨씬 더 복잡할 수 있다.SafeLock 속성은 (재적) Lock 클래스의 획득 및 해제 횟수가 지정된 메서드 호출 내에서 일치하도록 정책을 시행한다.물론, 이것은 잠금장치를 획득하는 방법 이외의 방법으로 잠금장치를 해제하는 것을 허용하지 않지만, 이것은 시험된 시스템이 달성하는 바람직한 목표일 가능성이 매우 높다.아래는 파라메트릭 컨텍스트 없는 패턴을 사용하는 이 속성의 사양이다.

③ 나사산 t, Lock l: S → S start(t) S binst(t) S end(t) S l.acquire(t) S l.release(t)

패턴은 각 스레드 및 잠금에 대해 중첩된 시작/끝 및 획득/해제 쌍의 균형 잡힌 시퀀스를 지정한다( ( ${\displaystyle \epsilon }$은(는) 빈 시퀀스임).여기서 시작과 끝은 프로그램의 모든 방법의 시작과 끝을 가리킨다(자체 획득 및 해제 호출은 제외).동일한 스레드에 속하는 경우에만 메서드의 시작과 끝을 연관시킬 필요가 있기 때문에 스레드의 파라메트릭이다.획득 및 해제 이벤트도 동일한 이유로 스레드에서 파라메트릭이 된다.한 Lock의 릴리즈와 다른 Lock의 인수를 연관시키고 싶지 않기 때문에 추가적으로 Lock의 파라메트릭이다.극단적으로, 잠금 기능이 있는 스레드(Trad)의 각 가능한 조합에 대해, 즉, 맥락 없는 구문 분석 메커니즘의 복사본이 있을 가능성이 있다. 이는 런타임 검증 시스템이 동일한 기능을 다르게 구현할 수 있기 때문에 직관적으로 다시 발생한다.예를 들어 나는 1{\displaystyle l_{1}}와 나는 2{\displaystyle l_{2}} 잠그는 시스템을 관자 놀이 부분이 있어 1{\displaystyle t_{1}}, 터 2{\displaystyle t_{2}}, t 3{\displaystyle t_{3}}, 쌍 &lt에 대한 속성 인스턴스를 유지하기 위해 가능하다는 데는 1{\displays.t핀란드 국영 방송 t_{1}}나는 1{\displaystyle l_{1}}>,<>는 과목은 1{\displaystyle t_{1}}, 나는 2{\displaystyle l_{2}}>,<>t 2{\displaystyle t_{2}}나는 1{\displaystyle l_{1}}>,<>t 2{\displaystyle t_{2}}나는 2{\displaystyle l_{2}}>,<>t 3{\displaystyle t_{3}}.나는 1{\displ$aystyle l_{1}},$ 그리고 < ${\displaystyle {}_{}}$ ${\displaystyle {3\mathrm{}}_{}}$ ${\$ l ${\displaystyle {2\mathrm{}}_{}}$ ${\$}}>.$$이 특성은 패턴이 지정된 올바른 동작 때문에 패턴과 일치하는 고장이 있는지 모니터링해야 한다.오른쪽 그림은 이 재산의 두 가지 위반을 나타내는 추적을 보여준다.그림에서 아래로 향한 단계는 방법의 시작을 나타내는 반면 위로 향한 단계는 끝이다.그림의 회색 화살표는 주어진 획득과 동일한 잠금 해제 사이의 일치를 보여준다.단순성을 위해 추적에는 스레드 한 개와 잠금 한 개만 표시된다.

연구 과제 및 애플리케이션

대부분의 런타임 검증 연구는 아래에 나열된 주제 중 하나 이상을 다룬다.

런타임 오버헤드 감소

실행 시스템을 관찰하면 일반적으로 일부 런타임 오버헤드가 발생한다(하드웨어 모니터는 예외일 수 있음).특히 생성된 모니터를 시스템과 함께 배치하는 경우 런타임 검증 도구의 오버헤드를 최대한 줄이는 것이 중요하다.런타임 오버헤드 감소 기법:

• 개선된 계측기.실행 시스템에서 이벤트를 추출하여 모니터로 전송하면 순진하게 실행될 경우 큰 런타임 오버헤드가 발생할 수 있다.도구가 명시적으로 기존 실행 로그를 대상으로 하지 않는 한, 우수한 시스템 계측은 모든 런타임 검증 도구에 중요하다.현재 사용 중인 기기에는 사용자 지정 또는 수동 계측에서 전문화된 라이브러리, 측면 지향 언어로의 컴파일, 가상 머신 확대, 하드웨어 지원 구축에 이르기까지 장단점을 가진 많은 기기 접근방식이 있다.
• 정적 분석과 결합.특히 컴파일러에서 발생하는 정적 및 동적 분석의 공통적인^{[citation needed]} 조합은 정적으로 방출될 수 없는 모든 요구사항을 모니터링하는 것이다.이중적이고 궁극적으로 동등한 접근방식은 런타임 검증에서 표준이^{[citation needed]} 되는 경향이 있는데, 즉 정적인 분석을 사용하여 그렇지 않으면 철저한 모니터링의 양을 줄이는 것이다.정적 분석은 모니터링할 속성 및 모니터링할 시스템에 대해 모두 수행할 수 있다.감시할 성질에 대한 정적 분석은 특정 사건이 감시할 필요가 없고, 특정 모니터의 생성이 지연될 수 있으며, 특정 기존 모니터가 결코 트리거되지 않아 쓰레기를 수거할 수 있다는 것을 밝혀낼 수 있다.모니터링할 시스템의 정적 분석은 모니터에 결코 영향을 미칠 수 없는 코드를 탐지할 수 있다.예를 들어, 위의 HasNext 속성을 모니터링할 때, 각 호출이 있는 코드의 계측기 부분이 필요하지 않다.i.next()어떤 경로에서든 호출에 의해 즉시 선행된다.i.hasnext()어느 쪽이 되느냐true(제어 흐름 그래프에 표시됨).
• 효율적인 모니터 생성 및 관리.위의 예와 같은 파라메트릭 속성을 모니터링할 때, 모니터링 시스템은 각 파라미터 인스턴스에 대해 모니터링되는 속성의 상태를 추적할 필요가 있다.그러한 사례의 수는 이론적으로 한계에 도달하지 못하고 실제로 엄청나게 많은 경향이 있다.중요한 연구 과제는 관찰된 사건을 어떻게 효율적으로 필요한 사례에 정확하게 배치할 것인가 하는 것이다.관련 과제는 그러한 인스턴스 수를 어떻게 작게 유지할 것인가(파견이 더 빠를 수 있도록), 다시 말해, 어떻게 하면 가능한 한 오랫동안 불필요한 인스턴스 생성을 피할 수 있는가, 그리고, 어떻게 하면 이미 생성된 인스턴스들이 불필요해지자마자 제거하는가 하는 것이다.마지막으로 파라메트릭 모니터링 알고리즘은 일반적으로 비모수 모니터를 생성하기 위해 유사한 알고리즘을 일반화한다.따라서 생성된 비모수 모니터의 품질은 결과 모수 모니터의 품질을 지시한다.그러나 다른 검증 접근법(예: 모델 점검)과는 달리, 런타임 검증에서는 상태 수나 생성된 모니터의 크기가 덜 중요하다. 사실, 어떤 시점에서는 오직 제한된 상태만이 가질 수 있지만, 일부 모니터는 위의 SafeLock 속성에 대한 상태와 같이 무한히 많은 상태를 가질 수 있다.일어난중요한 것은 모니터가 실행 시스템에서 이벤트를 수신할 때 상태로부터 다음 상태로 얼마나 효율적으로 전환되는가 하는 것이다.

속성 지정

모든 공식적인 접근방식의 주요한 실제적인 장애 중 하나는 사용자들이 사양을 읽거나 쓰는 방법을 배우기를 꺼리거나 모르거나 원하지 않는다는 것이다.교착 상태나 데이터 범위와 같이 규격이 암묵적인 경우도 있지만 대부분의 경우 그러한 규격을 생산해야 한다.특히 런타임 검증의 맥락에서 추가적인 불편함은 많은 기존 사양 언어가 의도된 속성을 포착할 수 있을 만큼 충분히 표현되지 않는다는 것이다.

• 더 나은 형식적 표현.런타임 검증 커뮤니티에서 상당한 양의 작업이 기존 사양 형식보다 런타임 검증을 위해 원하는 애플리케이션 도메인에 적합한 사양 형식 설계에 투입되었다.이 중 일부는 전통적인 형식에 대한 통사적 변화가 약간 있거나 전혀 없지만, 단지 의미론(예: 유한 추적 대 무한 추적 의미론 등)과 구현에 대한 변화(부치 오토마타 등 대신 최적화 유한 상태 기계)로 구성된다.다른 것들은 기존 형식주의를 런타임 검증에는 적합하지만 위의 예에서 보는 바와 같이 매개변수 추가와 같은 다른 검증 접근방법에 대해서는 쉽게 적용할 수 없는 특징으로 확장한다.마지막으로, 런타임 검증을 위해 특별히 고안된 사양 형식주의가 있으며, 이 도메인을 위해 최선을 다하려고 시도하며 다른 애플리케이션 도메인에 대해서는 거의 신경을 쓰지 않는다.런타임 검증을 위해 보편적으로 더 우수하거나 영역별로 더 나은 사양의 공식화를 설계하는 것은 주요 연구 과제 중 하나이며 앞으로도 계속 될 것이다.
• 양적 특성.다른 검증 접근방식에 비해 시스템 상태변수의 구체적 가치에 따라 런타임 검증이 동작할 수 있어 프로그램 실행에 대한 통계정보를 수집하고 이 정보를 활용해 복잡한 정량적 특성을 평가할 수 있다.우리가 이 능력을 충분히 활용할 수 있게 해줄 표현력 있는 속성 언어가 더 필요하다.
• 더 나은 인터페이스.비전문가가 재산명세서를 읽고 쓰는 것은 쉽지 않다.심지어 전문가들도 비교적 작은 시간적 논리 공식(특히 그들이 중첩된 "완전" 연산자를 가지고 있을 때)을 몇 분 동안 응시하는 경우가 많다.중요한 연구 영역은 사용자가 속성을 더 쉽게 이해하고, 쓰고, 심지어 시각화할 수 있도록 하는 다양한 사양 형식에 대한 강력한 사용자 인터페이스를 개발하는 것이다.
• 채굴 사양.사용자가 규격을 만들 수 있도록 어떤 도구 지원을 이용할 수 있든 간에, 그들은 특히 사소한 경우 규격을 전혀 작성하지 않으면 안 되는 것에 대해 거의 항상 더 기뻐할 것이다.다행히도, 그곳에는 재산에 대해 갖고 싶어하는 행동/이벤트를 올바르게 사용하는 많은 프로그램들이 있다.만약 그렇다면, 누군가가 그들로부터 원하는 속성을 자동으로 학습함으로써, 올바른 프로그램을 사용하고 싶어한다고 생각할 수 있다.자동 채굴된 규격의 전반적인 품질이 수동으로 생산된 규격보다 낮을 것으로 예상되더라도 후자의 시작점이나 버그(불량 규격은 잘못된 긍정이나 부정으로 바뀌는 경우)를 특별히 목적으로 하는 자동 런타임 검증 도구의 기초가 될 수 있다.종종 시험 중 허용된다.

실행 모델 및 예측 분석

오류를 엄격하게 탐지하는 런타임 검증기의 기능은 실행 추적 분석 기능에 따라 달라진다.모니터가 시스템과 함께 배치되는 경우, 계측은 일반적으로 최소 수준이며 실행 추적은 런타임 오버헤드를 낮게 유지하기 위해 가능한 한 단순하다.런타임 검증을 테스트에 사용할 경우 모니터가 실행 시스템의 보다 정교한 모델을 구축하고 분석하는 데 사용할 수 있는 중요한 시스템 정보로 이벤트를 증가시키는 보다 포괄적인 계측기를 제공할 수 있다.예를 들어, 벡터 시계 정보와 데이터 및 제어 흐름 정보로 이벤트를 증가시키면 모니터는 관찰된 실행이 하나의 가능한 인스턴스인 실행 시스템의 인과 모델을 구성할 수 있다.모델과 일치하는 다른 이벤트의 순열은 다른 나사산 인터리빙에서 발생할 수 있는 시스템의 실행 가능한 것이다.그러한 추론된 실행에서 (모니터링을 통해) 재산 위반을 탐지하면 모니터는 관찰된 실행에서 발생하지 않았지만 동일한 시스템의 다른 실행에서 발생할 수 있는 오류를 예측하게 된다.중요한 연구 과제는 가능한 많은 다른 실행 흔적을 구성하는 실행 추적에서 모델을 추출하는 것이다.

행동 수정

시험이나 철저한 검증과 달리, 런타임 검증은 시스템이 감지된 위반으로부터, 재구성, 마이크로리셋 또는 때로는 조정 또는 조향이라고 불리는 보다 미세한 개입 메커니즘을 통해 복구할 수 있도록 하는 약속을 지킨다.런타임 검증의 엄격한 프레임워크 내에서 이러한 기법의 구현은 추가적인 난제를 야기한다.

• 조치의 사양.사용자가 관련 없는 구현 세부사항을 알 필요가 없는 추상적인 방식으로 수행되도록 수정사항을 명시할 필요가 있다.또한 시스템의 무결성을 유지하기 위해 그러한 변경이 발생할 수 있는 경우를 명시할 필요가 있다.
• 개입 효과에 대한 추론.개입이 상황을 개선시키거나, 적어도 상황을 악화시키지는 않는다는 것을 아는 것이 중요하다.
• 작업 인터페이스.모니터링을 위한 계측기와 유사하게, 우리는 시스템이 조치를 취하도록 할 필요가 있다.호출 메커니즘은 필요에 따라 시스템의 구현 세부사항에 따라 달라진다.그러나 사양 수준에서는 어떤 조건에서 어떤 조치를 적용해야 하는지를 명시하여 사용자에게 시스템에 피드백을 제공하는 선언적인 방법을 제공할 필요가 있다.

관련업무

측면 지향 프로그래밍

런타임 검증의 연구자들은 프로그램 계측을 모듈화 방식으로 정의하기 위한 기법으로 측면 지향 프로그래밍을 사용할 수 있는 가능성을 인식했다.측면 지향 프로그래밍(AOP)은 일반적으로 교차 절단 우려의 모듈화를 촉진한다.런타임 검증은 당연히 그러한 관심사 중 하나이며 따라서 AOP의 특정 특성으로부터 이익을 얻을 수 있다.측면 지향적 모니터 정의는 대체로 선언적이며, 따라서 명령적 프로그래밍 언어로 작성된 프로그램 변환을 통해 표현되는 계측보다 추론하기가 더 간단한 경향이 있다.또한 정적 분석은 모든 계측기가 단일 측면 내에 포함되기 때문에 다른 형태의 프로그램 계측기보다 모니터링 측면에 대해 더 쉽게 추론할 수 있다.따라서 많은 현재 런타임 검증 도구는 표현형 고급 사양을 입력으로 사용하고 일부 측면 지향 프로그래밍 언어(예: SideonJ)로 작성된 출력 코드로 생성하는 사양 컴파일러 형태로 구축된다.

형식 검증과 조합

런타임 검증을 정확한 복구 코드와 함께 사용할 경우 프로그램 검증을 위한 귀중한 인프라를 제공할 수 있으며, 이는 후자의 복잡성을 현저히 낮출 수 있다.예를 들어 힙-소트 알고리즘을 공식적으로 검증하는 것은 매우 어려운 일이다.이를 검증하기 위한 한 가지 덜 어려운 기술은 정렬할 출력을 모니터링하는 것이다(선형 복잡성 모니터). 정렬되지 않은 경우 쉽게 검증 가능한 절차를 사용하여 정렬하는 것이다.결과적인 분류 프로그램은 이제 더 쉽게 검증할 수 있게 되었고, 힙 정렬에서 요구되는 유일한 것은 그것이 멀티셋으로 간주되는 원래의 요소들을 파괴하지 않는다는 것인데, 이것은 증명하기가 훨씬 쉽다.다른 방향에서 보면 형식적인 검증 대신 정적인 분석에 앞서 언급한 것처럼 형식적인 검증을 통해 런타임 검증의 오버헤드를 줄일 수 있다.실제로 완전한 런타임으로 시작할 수 있지만, 아마도 느린 프로그램일 것이다.그런 다음 컴파일러가 정적 분석을 사용하여 유형의 정확성 또는 메모리 안전성에 대한 런타임 검사를 수행하는 것과 마찬가지로 공식적인 검증(또는 정적 분석)을 사용하여 모니터를 방출할 수 있다.

커버리지 증가

전통적인 검증 접근방식에 비해 런타임 검증의 즉각적인 단점은 적용범위 축소다.이는 런타임 모니터를 시스템과 함께 배치하는 경우(속성이 침해될 때 실행될 적절한 복구 코드와 함께) 문제가 되지 않지만, 시스템에서 오류를 찾기 위해 사용할 경우 런타임 검증의 효과를 제한할 수 있다.오류 탐지를 위한 런타임 검증 범위를 늘리는 기법은 다음과 같다.

• 입력 생성.양호한 입력 집합(프로그램 입력 변수 값, 시스템 호출 값, 스레드 일람표 등)을 생성하면 시험의 효과를 엄청나게 높일 수 있다는 것은 잘 알려져 있다.이는 오류 검지에 사용되는 런타임 검증에도 해당하지만, 프로그램 코드를 사용하여 입력 생성 프로세스를 추진하는 것 외에도 런타임 검증에서 가능한 경우 속성 사양을 사용할 수 있으며, 모니터링 기법을 사용하여 원하는 동작을 유도할 수도 있다.이러한 런타임 검증의 사용은 런타임 검증 규격이 일반적으로 일반적인 목적이지만 반드시 테스트 이유로 조작된 것은 아니지만 모델 기반 테스트와 밀접하게 관련된다.예를 들어 위의 범용 안전하지 않은 에넘 속성을 테스트하려는 경우를 생각해 보십시오.시스템 실행을 수동적으로 관찰하기 위해 위에서 언급한 모니터를 생성하는 대신, 두 번째 e.nextElement() 이벤트를 생성하기 직전에 스레드를 동결하는 보다 스마트한 모니터를 생성할 수 있으며, 다른 스레드는 그 중 하나가 v.update() 이벤트를 생성하기를 희망하여 실행될 수 있다.오류가 발견된 경우
• 동적 기호 실행.상징적 실행 프로그램은 상징적으로 실행되고 감시된다. 즉, 구체적인 입력 없이 말이다.하나의 상징적인 시스템 실행은 많은 콘크리트 입력물을 포함할 수 있다.기성 제약조건 해결이나 만족도 점검 기법은 상징적 집행을 유도하거나 그 공간을 체계적으로 탐색하기 위해 종종 사용된다.기본 만족도 검사자가 선택 지점을 처리할 수 없는 경우, 그 지점을 통과하기 위해 구체적인 입력을 생성할 수 있다. 콘크리트와 상징적 실행의 이러한 조합을 콩쿨 실행이라고도 한다.

참고 항목

• 동적 프로그램 분석
• 프로파일링(컴퓨터 프로그래밍)
• 런타임 오류 감지
• RASP(Runtime Application 자체 보호)

참조