Certus: A domain specific language for confidence assessment in assurance cases

기술 요약: Certus – 보증 사례(Assurance Cases)의 신뢰도 평가를 위한 도메인 특화 언어

문제 정의
보증 사례(Assurance Cases, ACs)는 안전성이나 보안성과 같은 품질 속성을 임계 시스템이 충족함을 입증하기 위해 사용되는 구조화된 논증이다. 이러한 논증을 조직하기 위해 다양한 표기법(예: Goal Structuring Notation, Claims-Argument-Evidence)이 존재하지만, 이 논증의 타당성에 대한 '신뢰도(confidence)'를 결정하는 것은 여전히 과제로 남아 있다. 기존의 정량적 신뢰도 평가 방법(Quantitative Confidence Assessment Methods, CAMs)은 신뢰도에 수치적 값을 할당하려고 시도하지만, 채택 과정에서 상당한 장벽에 부착한다. 본 논문은 현재의 정량적 CAM이 직면한 다섯 가지 주요 한계점을 식별한다:

1. 해석(Interpretation): 수치적 출력값(예: 0.93)은 허용 가능한 임계값과 관련하여 해석하기 어렵고, 비전문가에 의해 오해될 소지가 있다.
2. 주관성(Subjectivity): 전문가에게 모호한 판단에 대해 정밀한 숫자를 할당하도록 강요하는 것은 인간 추론의 자연스러운 가변성을 무시하고 질적인 뉘앙스를 상실하게 한다.
3. 확장성(Scaling): Dempster-Shafer 이론과 같은 방식은 과도한 입력 파라미터(예: 리프 노드당 4개의 값)를 요구하여, 대규모 AC에 적용하기에는 비실용적이다.
4. 반박 요소(Defeaters): 의구심이나 부정적 신뢰도를 도입하는 변증법적 추론인 '반박 요소'를 적절히 처리하는 방법이 거의 없다.
5. 신뢰성(Trustworthiness): 복잡한 수학적 프레임워크는 종종 '블랙박스'로 작용하여 실무자의 신뢰를 떨어뜨리며, 이러한 방법들이 직관과 일치하는 결과를 생성한다는 것을 보여주는 경험적 검증이 부족하다.

방법론
본 논문은 **퍼지 집합론(fuzzy set theory)**과 프로그래밍 가능한 구문을 결합하여 이러한 한계점을 해결하도록 설계된 도메인 특화 언어(DSL)인 Certus를 소개한다.

• 퍼지 집합을 이용한 신뢰도 모델링: Certus는 사용자에게 정밀한 숫자 대신 언어적 용어(예: "높음", "매우 낮음", "확실함")를 사용하여 신뢰도를 할당할 수 있게 한다. 이러한 용어들은 도메인 $\beta = [0, 1]$ 상의 퍼지 집합(멤버십 함수)으로 모델링된다. 이 언어는 표준적인 정형 집합(zero, very low, low, med, high, very high, certain)을 포함하며, 사용자가 커스텀된 볼록(convex) 및 정규화된 퍼지 집합을 정의할 수 있도록 허용한다. 이 접근 방식은 공학적 판단에 내재된 모호함을 포착하면서도 수학적 엄밀성을 유지한다.
• 신뢰도 전파(Confidence Propagation): 신뢰도는 논증의 유향 비순환 그래프(DAG)에서 리프(증거)로부터 루트(최상위 클레임)로 재귀적으로 평가된다. Certus는 전파 규칙을 정의하기 위해 cases 표현식을 사용한다. 이 규칙들은 자식 노드의 퍼지 집합에 대한 조건( is, contains, overlaps, >, < 와 같은 연산자 사용)을 매칭하고, 이를 부모 노드의 결과 퍼지 집합으로 매핑한다.
• 반박 요소 처리: 반박 요소는 신뢰도를 감소시키는 부정적 전제로 모델링된다. Certus는 사용자가 정의한 전파 규칙(매크로에 의해 생성된 규칙 포함)이 반박 요소를 처리하기 위한 12가지 확립된 규칙을 준수하는지 확인하는 '사전 점검(pre-flight check)' 시스템을 통합하여, 변증법적 추론이 올바르게 통합되도록 보장한다.
• 매크로를 통한 확장성: 확장성을 지원하기 위해, Certus는 매개변수화된 전파 연산자와 매크로를 정의할 수 있게 한다. 매크로(Python과 같은 스크립팅 인터페이스를 통해 구현됨)는 논증 구조에 따라 cases 표현식으로 동적으로 확장되어, 대규모 AC에 필요한 수동 작업량을 줄여준다. 균형을 맞추고 여러 퍼지 집합을 병합하기 위해 내장된 FUSE 매크로가 제공된다.

주요 기여

1. Certus 언어: 퍼지 집합을 사용하여 AC 신뢰도를 모델링하고, 사용자 정의 표현식을 통해 구조화된 논증을 통해 신뢰도를 전파하는 최초의 DSL 제안.
2. 언어적 신뢰도의 정형화: 언어적 신뢰도를 제안하면서도 이를 정형화하지 않았던 이전 연구들과 달리, Certus는 노드에 퍼지 집합을 할당하고 전파 로직을 정의하기 위한 구문을 제공한다.
3. 반박 요소 통합: 논증 구조를 통해 "부정적 신뢰도"를 명시적으로 모델링하고 전파하는 메커니즘을 제공하며, 이는 확립된 반박 규칙에 의해 검증된다.
4. 투명성: 불투명한 수학적 공식 대신 단순하고 검사 가능한 표현식(cases 연산자)을 사용함으로써, Certus는 실무자들의 신뢰도와 이해도를 높이는 것을 목표로 한다.

결과
본 논문은 자동차용 적응형 크루즈 컨트롤(ACC)의 일부 단편에 Certus를 적용한 개념 증명 구현을 제시한다.

• 적용: 이 예시는 복잡한 추론 단계(증거와 반박 요소의 통합 포함)를 처리하기 위해 매개변수화된 연산자(invert, boundedInvert)와 FUSE 매크로를 사용하는 방법을 보여준다.
• 비교: 저자들은 Certus의 결과를 동일한 단편에 대한 기존의 베이지안 네트워크(BBN) 분석 결과와 비교하였다. BBN은 0.39의 수치적 신뢰도를 산출했다. Certus 방식은 이 값과 일치하는 결과(낮음에서 중간 정도의 신뢰도에 해당하는 퍼지 집합으로 해석됨)를 생성하였으며, 이는 Certus 방식이 기존의 정량적 접근 방식과 일치하면서도 다른 표현 방식을 제공함을 시사한다.

의의 및 주장
저자들은 Certus를 기존의 정량적 CAM을 대체하는 도구가 아니라, 특정 약점을 해결하기 위한 도구로 포지셔닝한다. 이 연구의 의의는 다음과 같다:

• 간극 해소: 전문가가 언어적으로 의미 있는 방식으로 신뢰도를 표현할 수 있게 함으로써(주관성 해결), 동시에 계산 및 전파가 가능한 능력(정량적 평가의 필요성 해결)을 유지한다.
• 신뢰도 향 향상: 전파 규칙을 명시적이고 검사 가능하게 만듦으로써, Certus는 현재 도구들의 '블랙박스' 성격을 완화하고자 한다.
• 확장성: 매크로와 재사용 가능한 연산자의 사용은 대규모의 복잡한 보증 사례에 대한 정량적 평가를 가능하게 하기 위함이다.

본 논문은 Certus가 현재 프로토타입임을 인정하며 겸허하게 결론을 맺는다. 향후 과제로는 정식 사양(formal specification) 작성, 가독성을 높이기 위한 그래픽 표현 개발, 그리고 실무자를 대상으로 한 사용성 및 신뢰성 검증을 위한 경험적 연구가 포함된다.