기술 요약: ACCESS – 안전 필수 시스템을 위한 보증 사례 중심 엔지니어링 (Assurance Case Centric Engineering of Safety-critical Systems)

1. 문제 정의

안전 필수 시스템(Safety-critical systems)은 정의된 맥락 내에서 작동하기 위해 안전성에 대한 명시적인 정당화가 필요합니다. 전통적으로 보증 사례(Assurance Cases)(증거에 의해 뒷받침되는 논거)는 수동으로 작성된 문서 형태로 존재하며, 길고 오류가 발생하기 쉬운 과정을 통해 평가됩니다. 시스템이 더욱 복밀해지고 서로 연결됨에 따라, 이질적인 엔지니어링 산출물 간의 검증, 타당성 확인(validation), 그리고 변경 영향 분석을 조율하는 개발 생애주기를 관리하는 것이 점점 더 어려워지고 있습니다.

나아가, **로봇 및 자율 시스템(RAS)**의 등장은 기존의 보증 접근 방식으로는 해결할 수 없는 과제를 제기합니다. RAS는 개방적이고 적응적이며, 최소한의 인간 개입만으로 운영 생애 동안 진화할 수 있는 보증 사례를 필요로 합니다. 현재의 방법론들은 다음과 같은 사항을 수행할 수 있는 충분한 모델 기반 토대를 갖추고 있지 않습니다:

1. 보증 사례를 다양한 엔지니어링 산출물(예: 아키텍처 모델, 안전 분석, 동작 모델)과 체계적으로 추적하는 것.
2. 보증 사례와 참조된 산출물들을 집합적으로 자동 평가하는 것.
3. 동적인 환경을 다루기 위해 안전 보증 활동을 개발 시점에서 런타임(runtime)으로 전환하는 것.

GSN(Goal Structuring Notation)이나 CAE(Claim-Argument-Evidence)와 같은 기존 표기법은 자동화되고 일관된 보증을 위해 필요한 외부 산출물로의 추적성을 네이티브하게 지원하지 않습니다.

2. 방법론: ACCESS

본 논문은 진화하는 모델 기반 보증 사례를 중심으로 안전 필수 시스템을 개발하는 엔지니어링 방법론인 ACCESS(Assurance Case Centric Engineering of Safety-critical Systems)를 제안합니다. ACCESS는 모델을 일급 객체(first-class artifacts)로 취급하는 모델 기반 시스템 엔지니어링(MBSE)의 원칙을 채택합니다.

이 방법론은 시스템 개발과 시스템 보증 활동을 조율하는 7가지 반복 단계를 구성합니다:

• 1단계: 보증 사례 계획: 시스템 기능, 하드웨어 플랫폼, 환경적 가정을 정의합니다. 예비 안전 목표를 도출하기 위해 고수준 안전 분석(예: Hara)을 수행합니다.
• 2단계: 보증 사례 생성: 시스템 아키텍처를 모델링하고 모듈형 보증 사례 모듈을 지정합니다. 할당된 요구사항에 대한 공개된 클레임(public claims)을 생성하고 피어 서브시스템(peer subsystems)에 대한 가정을 정의합니다.
• 3단계: 보증 사례 정교화: 서브시스템 안전 분석(예: FMEDA)을 수행하고 요구사항을 서브시스템에 할당합니다. 요구사항과의 추적성을 유지하면서 각 서브시스템에 대한 안전 논거를 개발합니다.
• 4단계: 엔지니어링 산출물 타당성 확인 및 검증: 형식적 의미론(formal semantics)을 가진 동작 모델(예: 상태 머신)을 생성합니다. 모델 분석 및 검증을 수행하여 요구사항이 충족되는지 확인하고 모델 무결성(예: 데드락 프리)이 유지되는지 확인합니다.
• 5단계: 보증 사례 평가: 시스템을 구현하고 시스템 수준의 검증 및 타당성 확인을 수행합니다. 보증 사례는 집합적으로 평가되며, 지원되지 않는 클레임이 발생하면 이전 단계의 재평가를 트리거합니다.
• 6단계: 동적 보증 사례로 변환: RAS를 위해 보증 사례의 특정 부분을 "동적" 형태로 변환합니다. 이는 운영 데이터를 엔지니어링 모델과 연결하는 런타임 데이터 드라이버를 정의하는 것을 포함하며, 이를 통해 보증 사례가 시스템의 현재 상태를 반영할 수 있도록 합니다.
• 7단계: 자동 런타임 평가: 런타임 데이터를 사용하여 동적 보증 사례에 대한 비침습적이고 자동화된 주기적 평가를 수행합니다. 유효성이 상실되면 시스템은 안전한 상태(safe state)로 전환될 수 있습니다.

3. 도구 지원: ACME

ACCESS를 지원하기 위해 저자들은 ACME(Assurance Case Management Environment)를 개발했습니다. ACME는 Eclipse Modeling Framework(EMF)와 Structured Assurance Case Metamodel(SACM)을 기반으로 구축된 모델 기반 프레임워크입니다.

ACME의 주요 기능은 다음과 같습니다:

• 추적성: 보증 사례 요소(Goals, Solutions, Contexts)에서 이질적인 엔지니어링 산출물(EMF 모델, Excel 스프레드시트, Isabelle theory 파일)로의 세밀한 추적을 지원합니다.
• 자동 검증: Epsilon Object Language(EOL)를 사용하여 엔지니어링 산출물을 보증 사례 제약 조건에 대해 검증하는 모델 쿼리를 실행합니다.
• 형식적 통합: Isabelle/HOL 서버와 연결하여 형식적 이론(예: 데드락 프리 증명)을 검증하고, 논리적 무결성 체크를 위해 보증 사례의 Isabelle/SACM 표현을 생성합니다.
• 동적 보증: 런타임 데이터를 보증 모델과 동기화하고 지속적인 평가를 수행하기 위한 런타임 데이터 드라이버 및 동적 안전 관리 시스템(DSMS) 지원을 제공합니다.

4. 사례 연구 및 결과

이 방법론과 도구는 **자율 무인 잠수정(AUV)**을 포함하는 사례 연구에 적용되었습니다. AUV의 안전 컨트롤러(Last Response Engine - LRE)는 RoboChart(CSP 의미론을 가진 그래픽 언어)를 사용하여 모델링되었습니다.

사례 연구의 주요 결과:

• 추적성: 연구팀은 Excel 스프레드시트의 FMEDA 결과, RoboChart 동작 모델, 그리고 Isabelle 형식 증명까지 안전 논거를 성공적으로 추적했습니다.
• 자동화: ACME는 Excel FMEDA 데이터에 대한 검증 규칙을 자동으로 실행하고 Isabelle 서버를 호출하여 형식 증명을 확인했습니다. 모델의 오류(예: 누락된 전이 또는 실패한 증명)가 보증 사례 에디터에 즉시 표시되었습니다.
• 런타임 적응: LRE 보증 사례가 동적 형태로 변환되었습니다. 런타임 센서 데이터(장애물 감지)가 모델과 동기화되었으며, 검증 규칙을 통해 센서 판독값이 안전 범위를 벗어나지 않는지 확인했습니다.
• 효율성 평가: 전원 공급 장치(시스템 A)와 항법 장치(시스템 B)에 대해 세 가지 접근 방식을 사용하여 비교 실험을 수행했습니다:
  1. 수동 (텍스트 기반).
  2. ACME 없는 모델 기반.
  3. ACME 지원을 받는 모델 기반.
  • 결과: 수동 방식은 훨씬 더 오래 걸렸으며(예: 시스템 A의 경우 505분), 런타임 보증을 지원할 수 없었습니다. ACME가 없는 모델 기반 방식은 시간을 단축했습니다(262분). ACME 지원을 받는 방식이 가장 효율적이었으며(~87분, 시스템 A 기준), 이는 개발 노력을 대폭 감소시킴을 보여주었습니다.
• 확장성: ACME는 최대 ~5,689개의 요소를 가진 모델을 성공적으로 처리했습니다. 그러나 확장성 테스트 결과, 쿼리를 위해 전체 EMF 모델을 메모리에 로드해야 하는 특성 때문에 모델 요소 수가 수백만 개에 달하면 메모리 오버플로 문제가 발생하는 것으로 나타났습니다.

5. 의의 및 기여

본 논문은 다음과 같은 주요 기여를 주장합니다:

1. ACCESS 방법론: 진화하는 보증 사례 모델을 중심으로 하는 핵심 시스템 엔지니어링 방법론으로, 개발과 런타임 보증 사이의 간극을 메웁니다.
2. 자동 평가: 개발 및 런타임 모두에서 보증 사례와 참조된 엔지니어링 산출물을 평가할 수 있는 프레임워크와 프로토타입 동적 관리 시스템을 제공합니다.
3. 형식적 통합: 다양한 형식 검증 결과(예: Isabelle로부터)를 보증 사례에 통합하고, 정리 증명(theorem proving)을 위해 자동화된 형식 보증 사례(Isabelle/SACM)를 생성하는 기능을 제공합니다.
4. 변경 영향 분석: 엔지니어링 산출물의 변경이 보증 사례에 미치는 영향을 자동화된 방식으로 분석합니다.
5. 실제 적용: 위 사항들을 AUV 사례 연구에 성공적으로 적용하여, 모델 기반 보증 중심 엔지니어링의 실현 가능성을 입증했습니다.

저자들은 ACCESS가 정적인 문서 기반 보증에서 동적인 모델 기반 보증으로의 전환을 가능하게 하며, 이는 불확실한 환경에 놓인 적응형 RAS의 안전을 위해 필수적이라고 강조합니다. 또한, 접근 방식이 효율성과 커버리지를 개선하지만, 확장성 한계를 해결하고 검증 규칙 정의를 위한 기술적 장벽을 낮추기 위해(예: 제약된 자연어 지원) 향후 연구가 필요하다고 언급했습니다.