Automated Repair of Requirements for Cyber-Physical Systems in Simulink Requirements Tables

기술 요약: Simulink Requirements Tables에서의 사이버 물리 시스템을 위한 요구사항 자동 수정

문제 정의

복잡한 사이버 물리 시스템(CPS)의 개발은 시스템 구현과 그에 따른 요구사항이 지속적이고 종종 독립적으로 진화하는 과정을 포함한다. 이러한 독립성은 시스템 업데이트(예: 성능 향상 또는 하드웨어 변경)가 기존 요구사항을 쓸모없게 만들거나 부적절하게 만드는 미스얼라인먼트(misalignment) 위험을 초래한다. 자동 프로그램 수정(APR)은 시스템을 수정함으로써 미스얼라인먼트를 해결하지만, 이는 요구사항이 올바르다는 전제하에 작동하며, 요구사항이 결함이 있거나 구식이며 불충분할 수 있는 안전 필수 분야에서는 이 전제가 빈번히 실패한다.

기존의 APR 기술은 다음과 같은 이유로 CPS 요구사항을 수정하기에는 부적합하다:

1. 도메인 불일치: APR은 일반적으로 명령형 코드나 고수준 모델을 대상으로 하지만, CPS 요구사항는 대개 시간 기반의 실수 신호에 대한 선언적 논리식이다.
2. 입도(Granularity): 기존 방식은 거친 입도의 수정(블록 추가/제거)을 수행하거나, 수치적 추론 능력이 최소화된 상태에서 논리식의 구조적 조작에 국한된다.
3. 컨텍스트: APR은 단독으로 존재하는 선언적 요구사항에서 사용할 수 없는 컨텍스트 단서(예: 주변 코드)에 의존한다.

결과적으로, 보완적인 전략인 **자동 요구사항 수정(Automated Requirement Repair)**이 필요하다. 이는 시스템 자체를 변경하는 대신, 진화된 시스템 동작에 맞추어 요구사항을 수정하는 방식이다.

방법론

저자들은 실행 데이터(trace suites)를 활용하여 MATLAB Simulink® Requirements Tables (RT) 언어로 명시된 미스얼라인된 요구사항을 수정하는 프레임워크를 제안한다.

1. 수정 문제의 정형화:

• 입력: 트레이스 슈이트 $TS$(시간에 따른 입출력 트레이스의 집합)와 잘못된 요구사항$r_0$.
• 출력: $TS$에 대해 올바른(모든 트레이스에 의해 만족되는) 동시에 특정 바람직함 기준에 따라 최적화된 수정된 요구사항$r^*$.
• 의미론(Semantics): 프레임워크는 RT의 정량적 의미론을 활용하여 요구사항에 대한 만족도를 할당한다. 요구사항은 모든 트레이스에 대해 만족도가 0 이상일 때 올바른 것으로 간주된다.

2. 다목적 최적화 프레임워크:
수정 과정은 다목적 최소화 문제로 구성된다. 프레임워크는 **정확성(Correctness)**과 네 가지 바람직함 차원(Desirability Dimensions) 사이의 균형을 맞추는 파레토 최적(Pareto-optimal) 수정 세트를 탐색한다:

• 의미론적 무결성 ($d_{sem}$): 수정된 요구사항이 비자명(non-trivial, 항진식이나 모순이 아님)하고 도메인 속성(예: 단위 호환성)과 일치하도록 보장한다.
• 구문적 유사성 ($d_{syn}$): 불필요한 복잡성을 피하기 위해 원래 요구사항과 수정된 요구사항 사이의 구조적 거리(예: 트리 편집 거리)를 측정한다.
• 만족 범위 ($d_{sat}$): 요구사항의 경계가 관측된 동작으로부터 얼마나 떨어져 있는지(크기)와 전제 조건이 위반되는 빈도(폭, 공허한 참을 유발하는 정도)를 평가하여, 요구사항이 지나치게 넓거나 제한적이지 않고 정보가 풍부하도록 한다.

3. 탐색 알고리즘:
프레임워크는 다음과 같이 구성된 사용자 정의 가능한 탐색 루프(평가 시 진화 알고리즘을 사용하여 구현됨)를 채택한다:

• 후보 생성: RT 문법에 대한 변이(mutation) 및 교차(crossover) 연산자를 통해 새로운 요구사항을 생성한다.
• 평가: 각 후보에 대한 정확성 및 바람직함 적합도 값을 계산한다.
• 선택: 비지배 정렬(non-dominated sorting)을 사용하여 다음 세대를 위한 최적의 후보를 선택한다.

주요 기여

1. 문제 정의: Simulink RT에서 명시된 CPS를 위한 요구사항 수정 문제를 공식적으로 정의하고, 트레이스 슈이트에 대한 정량적 만족도 개념을 도입하였다.
2. 바람직함 프레임워크: 단순한 정확성을 넘어 의미론적 무결성, 구문적 유사성, 만족 범위를 포함하는 다차원적인 수정 품질 평가 프로토콜을 제시하였다.
3. 사용자 정의 가능 프레임워크: 기존 APR 기술에는 부족한, 실수 기반의 시간 기반 신호에 대한 선언적 요구사항을 처리할 수 있는 일반적인 수정 프레임워크를 제공한다.
4. 실증적 평가: Toyota, MathWorks, Lockheed Martin의 모델을 포함한 6개의 실제 사례 연구(12개 요구사항)를 통해 광범위한 평가를 수행하였다.

결과

저자들은 7가지 변형된 프레임워크를 사례 연구에 걸쳐 평가하였다:

• 정확성 vs. 바람직함: 연구 결과, 발견된 올바른 수정본의 수와 바람직함 점수 사이에 트레이드오프 관계가 있음이 밝혀졌다. 별도의 목적 함수를 사용하는 전략(NoAgg)이 가중 합산 전략(WeiSum)보다 더 많은 양의 올-바르고 의미론적으로 온전한 수정본을 생성했으나, 후자가 발견된 수정본들에 대해 약간 더 나은 바람직함 점수를 나타냈다.
• 항진식 검사: 의미론적 무결성을 위해 샘플링 기반 접근 방식보다 정밀한 SMT 기반의 정확한 검사를 사용하는 것이 선호되었으나, 두 방식 모두 유사한 양의 올바른 수정본을 생성했다.
• 탐색 파라미터: 진화 탐색에서 자손(offspring)의 수를 늘리면 실행 시간은 증가하지만, 고품질(올바르고 의미론적으로 온전한)의 수정본을 찾는 능력이 크게 향상되었다.
• 유용성: 전문가 분석 결과, 프레임워크가 유용하고 비자명한 수정을 생성할 수 있음이 확인되었다. 대부분의 사례 연구에서 구문적 유사성이나 만족 범위를 기준으로 정렬했을 때, 상위 3개 후보 내에서 유용한 수정본이 발견되었다.
• 절제 연구(Ablation Study): 단일 바람직함 차원(의미론적 무결성, 구문적 유사성, 만족 범위)을 제거하면 전체적인 수정 품질이 저하되었으며, 이는 효과적인 수정을 위해 세 가지 차원이 모두 필요함을 입증한다.

의의 및 주장

본 논문은 데클러러티브(declarative) CPS 요구사항을 위한 자동 수정의 공백을 성공적으로 메운다고 주장한다. 시스템을 고치는 대신 요구사항을 고치는 데 초점을 맞춤으로써, 이 접근 방식은 시스템 수정이 불가능하거나 요구사항 자체가 미스얼라인먼트의 원인일 때 실행 가능한 대안을 제공한다.

저자들은 본 연구가 '언제' 요구사항을 수정할지 아니면 시스템을 수정할지에 대한 결정 자체를 자동화하는 것이 아니라, 엔지니어가 내린 결정을 실행할 수 있는 기술적 수단을 제공한다는 점을 강조한다. 이 프레임워크는 실수 기반의 시간 기반 신호를 처리할 수 있는 능력과, 수학적 정확성뿐만 아니라 실질적인 바람직함 지표(예: 자명한 해 방지 및 도메인 일관성 유지)를 수정 과정에 통합했다는 점에서 의의가 있다. 결과는 수학적으로 실행 트레이스에 대해 정확할 뿐만 아니라, 의미론적으로 유의미하고 원래 명세와 구문적으로 근접한 요구사항을 자동으로 도출하는 것이 가능하다는 것을 보여준다.