Automated LTL Specification Generation from Industrial Aerospace Requirements

1. 문제 정의 (Problem Statement)

항공우주 분야의 안전-중요 (safety-critical) 소프트웨어 개발 및 검증 과정에서 선형 시간 논리 (Linear Temporal Logic, LTL) 는 복잡한 시스템 속성을 명세하는 데 널리 사용됩니다. 그러나 산업 현장에서는 다음과 같은 심각한 병목 현상이 존재합니다.

• 수동 변환의 한계: 자연어 (Natural Language, NL) 요구사항을 정밀한 LTL 속성으로 변환하는 과정은 노동 집약적이며 오류가 발생하기 쉽습니다. 이는 항공우주 제어 공학과 형식 방법 (Formal Methods) 에 대한 희귀한 전문 지식을 모두 요구하기 때문입니다.
• 기존 도구의 실패: 최근 등장한 NL-to-LTL 도구들 (NL2SPEC, NL2TL 등) 은 합성 벤치마크에서는 성과를 보이지만, 실제 산업 문서에서는 실패합니다. 그 이유는 다음과 같습니다.
  1. 전문 용어의 복잡성: 도메인 특유의 전문 용어 (Jargon) 와 약어가 명확하지 않게 사용됨.
  2. 암시적 구조: 시간적 (Temporal) 및 논리적 관계가 텍스트에 명시적으로 드러나지 않음 (예: "스위치"라는 단어는 다음 시간 단계의 상태 전이를 의미함).
  3. 문맥 단절: 요구사항이 인터페이스 정의서 (Interface Description) 나 호출 조건과 같은 별도의 엔지니어링 아티팩트와 분리되어 있어, LLM 이 이를 연결하지 못함.

2. 제안 방법론: AeroReq2LTL 프레임워크

저자들은 이러한 문제를 해결하기 위해 AeroReq2LTL이라는 자동화 프레임워크를 제안합니다. 이 프레임워크는 대규모 언어 모델 (LLM) 의 추론 능력을 활용하되, 두 가지 핵심 산업 혁신을 통해 도메인 지식을 통합합니다.

A. 전체 워크플로우 (Dual-stream Context Reconstruction)

1. 이중 스트림 문맥 재구성 (Dual-stream Context Reconstructing):
   • 타겟 스트림 (Target Stream): 요구사항 문단 전체를 추출하여 기능적 논리와 호출 조건 (예: 제어 주기) 을 보존합니다.
   • 지식 스트림 (Knowledge Stream): 인터페이스 정의서 (Interface Description) 에서 신호 이름, 데이터 타입, 유효 범위 등의 메타데이터를 추출합니다.
2. NL-to-TNL 재작성 (Semantic Rewriting): 자연어를 템플릿 기반 자연어 (Templated Natural Language, TNL) 로 변환합니다.
3. TNL-to-LTL 변환 (Deterministic Synthesis): TNL 을 결정론적 규칙을 통해 LTL 명세로 변환합니다.

B. 핵심 구성 요소

1. SpaceKG (Space Knowledge Graph):

   • 목적: 전문 용어의 분해 (Fragmentation) 를 방지하고 정확한 원자 명제 (Atomic Propositions) 로 매핑합니다.
   • 기능: 인터페이스 정의서에서 추출한 변수 (예: dwCount, flagSP) 와 값 (예: 0.15°/s) 을 기반으로 도메인 용어 (예: "각속도") 를 코드 수준의 정확한 변수로 정규화합니다.
   • 효과: LLM 이 "태양 감지"를 임의의 단어가 아닌 실제 변수 flagSP 로 인식하도록 'Grounding'을 수행합니다.

2. SpaceRDL (Space Requirement Description Language) & TNL:

   • 목적: 암시적인 시간적 제약과 논리적 관계를 명시화합니다.
   • 기능: 요구사항을 workmode, condition, timing, action 등 고정된 필드를 가진 구조화된 템플릿 (TNL) 으로 변환합니다.
   • 효과: "다음 단계에서 전환된다"와 같은 암시적 시간적 관계 (Next operator, X) 를 TNL 단계에서 명시적으로 드러내어, LLM 이 LTL 변환 시 시간 연산자를 누락하거나 잘못 배치하는 것을 방지합니다.

3. 주요 기여 (Key Contributions)

1. 산업용 자동화 프레임워크 개발: 실제 항공우주 요구사항 문서에서 LTL 명세를 생성하는 첫 번째 자동화 프레임워크인 AeroReq2LTL 을 제안했습니다.
2. 도메인 특화 지식 통합 (SpaceKG): 인터페이스 아티팩트를 자동으로 분석하여 기술 용어를 코드 레벨의 변수로 매핑하는 데이터 사전 방식을 도입했습니다.
3. 구조적 모호성 제거 (SpaceRDL): 자연어의 모호성을 제거하기 위해 도메인 논리에 기반한 템플릿 언어를 설계하여, LLM 의 추론을 구조화된 중간 표현 (TNL) 으로 유도했습니다.
4. 실제 산업 데이터셋 검증: 실제 우주선 제어 소프트웨어 (ACS-LEOS) 의 79 개 생산 요구사항을 대상으로 한 평가 및 검증 도구 (TRACE) 와의 연동 성공을 입증했습니다.

4. 실험 결과 (Evaluation Results)

실제 우주선 자세 제어 소프트웨어 (SSCS 모듈) 의 79 개 요구사항을 대상으로 평가进行了.

• 성능 지표:
  • 정확도 (Precision): 85% (GPT-4o 기반)
  • 재현율 (Recall): 88% (GPT-4o 기반)
  • 이는 기존 벤치마크 도구 (NL2SPEC, NL2LTL 등) 의 성능 (약 30~60% 대) 을 크게 상회합니다.
• Ablation Study (성분 제거 실험):
  • SpaceKG 제거 시: 정확도 69%, 재현율 70% 로 하락 (전문 용어 매핑 오류 발생).
  • SpaceRDL 제거 시: 정확도 52%, 재현율 54% 로 급격히 하락 (시간적 구조 및 논리 연산자 누락/오류).
  • 이는 두 구성 요소가 모두 정확도에 필수적임을 증명합니다.
• 검증 도구 연동: 생성된 LTL 명세는 TRACE(실행 경로 기반 검증 도구) 에 직접 입력되어 67 개 명세 중 63 개가 성공적으로 검증되었습니다.

5. 의의 및 결론 (Significance and Conclusion)

• 실용적 가치: 형식 방법의 산업 적용 장벽을 낮추고, 수동 명세화 노력을 크게 줄여 항공우주 소프트웨어의 검증 효율성을 극대화합니다.
• 기술적 혁신: LLM 을 단순히 텍스트 변환기가 아닌, 도메인 지식 (SpaceKG) 과 구조적 템플릿 (SpaceRDL) 을 통해 제어된 엔지니어링 도구로 변모시켰습니다.
• 확장성: 항공우주 분야를 넘어 자동차, 의료 등 유사한 문서 표준을 가진 다른 안전-중요 시스템으로의 확장이 가능합니다.

결론적으로, 이 연구는 자연어 요구사항에서 형식 명세로의 변환을 단순한 텍스트 처리가 아닌, 엔지니어링 아티팩트와 도메인 논리가 통합된 체계적인 공학적 프로세스로 재정의함으로써, 산업 현장에서의 형식 검증 도입을 현실화했습니다.