제7부 자율성·군집
7.8 런타임 보증(RTA)과 정형 검증
7.8.1 이 장에서 배우는 것 / 선수 지식 / 특히 중요한 독자
머신러닝(ML, machine learning)이나 복잡한 최적화로 만든 비행 기능은 기존 소프트웨어 보증으로 옳다고 보이기 어렵다. 시험만으로 높은 안전 수준을 입증할 수 없다는 것은 1.16.7이 계산했다. 이 장은 그 빈자리를 메우는 두 도구를 다룬다. 런타임 보증(RTA, run-time assurance)은 운용 중에 상태를 감시해 기체가 안전한 범위 밖으로 나가지 못하게 묶는 구조다. 정형 검증(formal verification)은 모형이나 코드의 성질을 수학으로 증명하는 방법이다. 둘은 경쟁하지 않는다. 작은 것을 증명하고, 그 작은 것으로 큰 것을 감싼다.
배우는 것:
- RTA의 구조 — 복잡 기능·회복 기능·안전 감시기·전환기로 이루어진 Simplex 구조와 ASTM F3269-21의 틀, 보증이 감시기 쪽으로 옮겨 가는 이유.
- 안전 경계의 설계 — 허용 집합·회복 가능 집합·전환 경계의 관계, 도달 가능 집합과 제어 장벽 함수의 직관.
- 전환 시간 예산 — 감시 지연·전환·복구 기동이 경계 폭을 정하는 식과, 제어 수준·지오펜스 수준·사람이 회복하는 구조의 차이.
- Simplex 전환 시뮬레이션 — 지연 버짓을 틀리면 무엇이 일어나고, 공통 원인이 왜 하한을 형성하는가.
- 정형 검증과 신경망 검증 — 모형 검사·정리 증명·추상 해석이 증명하는 것과 못 하는 것, 신경망 검증의 규모와 사양의 벽.
- 인증과의 연결 — 보증 수준의 배분, 운용 위험 평가의 완화 수단, AI 인증 동향으로 이어지는 길.
선수 지식: 독립 감시와 공통 원인의 식은 1.16.7.1, 다중화의 공통 원인과 비유사 설계는 2.5.4.3·2.5.9, 루프 주기와 지연의 기준값은 2.2.5, 완충 폭 계산은 2.6.4.2, 안전 모니터의 세 방식은 2.10.8.2, 필요 탐지 거리의 식과 ACAS Xu의 신경망 검증 사례는 2.14.5·2.14.9.2다. 수식은 미분과 확률 수준이다.
특히 중요한 독자: 엔지니어는 7.8.4~7.8.6과 7.8.9의 워크스루를 본다. 인증 담당자는 7.8.3·7.8.7·7.8.8·7.8.13을 본다. 무엇을 증거로 낼 수 있는지가 거기 있다. 정책·사업 담당자는 7.8.2와 7.8.10·7.8.11만 읽어도 된다.
기준 시점과 경계. 이 장은 2026년 10월을 기준으로, 지식은 2026년 중반까지 반영했다. 수치는 일반적 모형, 교육용 가정이며 특정 제품의 성능이 아니다. 계산과 시뮬레이션은 파이썬 표준 라이브러리(
math·random, 고정 시드)로 했다(mil-uam/fig-src/7.8-model.py·7.8-calc.py). ASTM F3269는 유료 표준이라 공개 요약과 목차 수준에서만 작성했다. 제조사·정부의 주장 수치는(공개 주장치), 확인하지 못한 사실은(확인 필요)로 표시했다. 이 장은 비행 안전의 보증 구조를 다루며, 무기 운용 기능의 자율화는 다루지 않는다(규범은 19.3).
7.8.2 개념·직관 — 증명할 수 없는 것을 증명할 수 있는 것으로 감싼다
운전 교습 차량에는 조수석에 보조 브레이크가 있다. 학생(복잡하고 예측하기 어려운 운전자)이 대부분을 몰고, 강사(단순하고 믿을 만한 감시자)는 위험해질 때만 브레이크를 밟는다. 학생이 옳게 운전한다는 증명은 없다. 그래도 강사가 늦지 않게 밟는다면 차는 안전하다. RTA는 이 구조를 기체에 옮긴 것이다.
기존 보증은 설계 시점 보증(design-time assurance)이다. 요구에서 코드까지 추적하고 시험해 "이 소프트웨어는 옳다"를 보인다(8.8). 학습된 신경망에는 요구를 한 줄씩 대응시킬 코드가 없고, 입력 공간이 넓어 시험이 포괄하지 못한다. RTA는 질문을 바꾼다. "복잡 기능이 옳은가" 대신 "복잡 기능이 무엇을 내든 기체가 안전 범위를 벗어나지 않는가"를 묻는다. 이 질문은 감시기와 회복 기능만 증명하면 답할 수 있다.
RTA가 성립하려면 세 조건이 필요하다.
- 경계를 계산할 수 있어야 한다. 안전 범위를 상태의 단순한 식(거리·속도·고도·자세)으로 나타낼 수 있어야 감시기가 빠르게 판정한다.
- 회복 기능이 그 경계에서 실제로 안전하게 만들 수 있어야 한다. 멈출 수 없는 고정익에 "정지"는 회복이 아니다.
- 감시기와 회복 기능이 복잡 기능과 같은 원인으로 틀리지 않아야 한다. 같은 센서·같은 추정·같은 전원을 사용하면 함께 속는다(1.16.7.1의 $\beta$).
세 축의 요구는 이렇게 다르다.
| 축 | RTA가 감싸는 것 | 주된 요구 |
|---|---|---|
| 군용 드론 | 학습 기반 임무 자율·편대 비행 같은 고성능 기능(운용 개념 수준) | 비행 영역·지오펜스·공중 충돌 회피의 보장, 링크 없이 도는 감시, 군 감항(12.3) |
| 민간 UAS | 오픈소스 오토파일럿·영상 기반 회피·학습 기반 착륙 | 운용 위험 평가에서 완화 수단으로 인정받는 근거(17.17), 낮은 비용 |
| AAM | 인증 대상 비행 제어에 들어오는 학습 기능, 자율 비행의 단계적 도입 | 승객 안전 수준의 증거, 인증 당국과의 기준 합의(20.5·20.10) |
7.8.3 RTA의 구조 — Simplex와 ASTM F3269
7.8.3.1 구성 요소
이 구조의 원형은 Simplex다. Seto·Krogh·Sha·Chutinan(1998)이 운용 중인 제어계에 검증되지 않은 새 제어기를 안전하게 올리는 방법으로 제안했고, Sha(2001)가 "단순함으로 복잡함을 다스린다"는 이름으로 정리했다. 고성능 제어기·안전 제어기·결정 모듈의 세 부분이다. 오늘의 RTA 용어로 나타내면 아래 그림이 된다.
| 구성 요소 | 하는 일 | 보증 요구 | 흔한 실패 |
|---|---|---|---|
| 복잡 기능(complex function) | 평소에 기체를 몬다. 학습 기반·최적화·복잡한 논리 | 낮아도 된다(구조로 격리될 때) | 분포 밖 입력, 사양에 없는 행동 |
| 회복 기능(recovery function) | 경계에서 기체를 안전 상태로 데려간다 | 높다 | 운용 설계 영역(ODD, operational design domain) 일부에서 회복 불가(강풍·고정익의 정지) |
| 안전 감시기(safety monitor) | 상태와 복잡 기능의 명령을 보고 경계를 판정 | 높다 | 지연을 빠뜨린 경계, 같은 센서를 공유 |
| 전환기(RTA switch) | 한 순간에 한 명령만 통과시킨다 | 높다 | 전환 때 명령 급변, 되돌아가는 조건의 모호함 |
| 입력 관리(input manager) | 센서·상태를 세 기능에 나눠 준다 | 높다 | 감시기에 복잡 기능의 추정값을 넘겨 독립성이 깨짐 |
ASTM F3269의 공개 요약은 사람도 복잡 기능이나 회복 기능이 될 수 있다고 적는다. 원격 조종사가 평소에 몰고 자동 회복이 담당하는 구조, 자율 비행을 원격 조종사가 감시하다 넘겨받는 구조가 모두 RTA다. 다만 사람이 회복 기능이면 지연이 초 단위가 되고 경계가 크게 넓어진다(7.8.5).
유인기에도 사례가 있다. 미 공군 F-16의 자동 지면 충돌 회피 체계(Auto-GCAS)는 지형 자료와 항법으로 회복 기동이 가능한 마지막 순간을 계산하고, 그때만 조종권을 가져가 기체를 상승시킨 뒤 돌려준다. 2014년부터 개조 장착이 시작되었고, 미 공군 연구소(AFRL)는 2021년 무렵 조종사 11명·기체 10대를 구했다고 발표했다 (공개 주장치, 이후 집계 확인 필요). "마지막 순간에만 개입한다"는 원칙이 RTA의 전환 경계와 같다.
7.8.3.2 ASTM F3269-21의 틀
ASTM F3269-21(Standard Practice for Methods to Safely Bound Behavior of Aircraft Systems Containing Complex Functions Using Run-Time Assurance)은 ASTM F38 위원회의 실무 관행 표준이다. 2017년 판(F3269-17)을 2021년에 개정했고, 2026년 10월 ASTM 판매 페이지 기준으로 F3269-21이 현행이다. 공개 요약에서 확인되는 요지는 다음과 같다.
- 설계 시점 보증의 대안으로 RTA 체계를 개발하는 구조적 틀을 준다. 기존 보증 산출물(DO-178C·DO-254)을 얻기 어려운 기능을 겨냥한다.
- 구성 요소로 입력 관리·안전 감시기·RTA 전환기·회복 기능을 두고, 인터페이스·커버리지·사건 시간(event timing)을 다룬다. 사건 시간은 이 장의 전환 시간 예산과 같은 관심사다.
- 구성 요소의 보증 수준은 안전성 평가가 정한다. 그 근거로 SAE ARP4754A·ARP4761과 ASTM F3178을 든다.
- 모든 크기·등급의 UAS를 염두에 두고 만들었고, 유인기와 지상 체계에도 적용할 수 있다. 하드웨어·소프트웨어 통합은 다루지 않는다.
본문의 세부 요건은 이 장이 옮기지 않았다. 이 장의 식과 수치는 표준의 값이 아니라 원리로 계산한 교육용 값이다.
7.8.3.3 보증은 어디로 옮겨 가는가
RTA는 보증을 없애지 않고 옮긴다. 복잡 기능의 보증 부담을 줄이는 대신 감시기·회복 기능·전환기를 높은 보증 수준으로 만든다. 이것이 상용 연산 모듈(2.9.10.2)이나 오픈소스 스택(2.10.11의 ①)을 사용할 때의 논리다. 복잡 기능의 개발 보증 수준을 실제로 얼마나 낮출 수 있는지는 구조의 독립성을 근거로 안전성 평가와 인증 당국의 합의가 정한다(8.4·20.5) (사례별, 일반 규칙 확인 필요).
옮겨 간 보증의 크기는 1.16.7.1의 식이 말한다. 복잡 기능이 위험한 명령을 낼 확률을 $p$, 감시기가 독립적으로 놓칠 확률을 $q$, 둘이 같은 원인으로 함께 틀리는 비율을 $\beta$라 하면 RTA를 거친 위험은 $p\,[(1-\beta)q+\beta]$다. RTA는 $q$를 작게 만드는 장치이고, $\beta$는 독립성 설계가 정한다. 2.5.4.3이 보인 대로 $\beta$가 하한을 형성한다. RTA에서 흔한 공통 원인과 분리 방법은 다음과 같다.
| 공유하는 것 | 함께 틀리는 예 | 분리 방법 |
|---|---|---|
| 같은 인지 결과 | 감시기가 복잡 기능의 장애물 지도를 그대로 사용한다 | 감시기 전용 센서와 단순 처리(7.1) |
| 같은 원리의 센서 | 유리면·얇은 전선을 카메라와 LiDAR가 함께 놓친다 | 원리가 다른 센서(레이더·초음파), ODD에서 해당 조건 제외 |
| 같은 항법 해 | GNSS 스푸핑이 복잡 기능과 감시기의 위치를 함께 옮긴다 | 무결성 감시(4.4.5.4), 대체 항법(4.7) |
| 같은 처리기·전원 | 과열·전압 강하로 둘이 함께 멈춘다 | 별도 처리기·보조 전원(2.6.8.2) |
| 같은 사양 해석 | 경계를 정한 요구서의 오류가 둘에 함께 들어간다 | 다른 팀, 정형 사양(7.8.7), N-버전의 교훈(2.5.9) |
7.8.4 안전 경계의 설계 — 전환이 늦지 않으려면
7.8.4.1 세 개의 집합
결론부터: 감시기는 기체가 위험해진 뒤가 아니라 "지금 넘기면 아직 구할 수 있는" 마지막 지점에서 넘겨야 한다. 그 지점은 세 집합으로 정한다.
- 허용 집합 $\mathcal S$ — 안전 제약을 만족하는 상태. 예: 벽과의 거리 $d\ge d_{\min}$.
- 회복 가능 집합 $\mathcal R\subset\mathcal S$ — 회복 기능을 지금 켜면 앞으로도 $\mathcal S$ 안에 머무는 상태.
- 전환 경계 — $\mathcal R$의 가장자리에서 지연 동안 기체가 갈 수 있는 만큼 안쪽으로 당긴 선. 감시기는 상태가 이 선에 닿으면 넘긴다.
1차원 접근에서는 식이 손에 잡힌다. 감속 능력 $a$로 멈추는 기체의 회복 가능 집합은 $d-d_{\min}\ge v^{2}/(2a)$다. 감시·전환·응답의 지연 합을 $T$라 하면 감시기는 다음이 성립할 때 넘긴다.
$$d-d_{\min}\ \le\ v\,T+\frac{v^{2}}{2a}+e$$
$e$는 거리 측정의 오차 여유다. 이 식은 지연 동안 복잡 기능이 속도를 유지한다고 가정했다. 증명을 하려면 최악을 가정해야 한다. 지연 동안 복잡 기능이 가속도 $a_{+}$로 가속하면 경계는 $vT+\tfrac12 a_{+}T^{2}+(v+a_{+}T)^{2}/(2a)$로 넓어진다. $a=a_{+}=4$ m/s², $T=0.25$ s에서 계산하면 10 m/s의 경계가 15.0 m에서 17.75 m로 2.75 m 늘어난다. 증명은 최악을 가정해 보수적이고, 시험은 관찰한 행동에 맞춰 좁다. 이 차이를 어디서 받아들일지가 설계 판단이다.
7.8.4.2 도달 가능 집합 — 차원이 늘면
여러 차원에서는 $\mathcal R$을 손으로 작성할 수 없다. 일반적인 방법은 역방향 도달 가능 집합이다. "회복 기능이 무엇을 해도 제약 위반을 피할 수 없는 상태"의 집합을 구하고 그 바깥을 회복 가능 집합으로 둔다. 해밀턴-야코비 방정식을 상태 격자 위에서 푸는 방법(Mitchell·Bayen·Tomlin, 2005)이 대표적이다.
문제는 차원의 저주다. 축마다 100칸으로 나눈 격자의 칸 수는 다음과 같다(칸당 8바이트).
| 상태 차원 | 예 | 칸 수 | 메모리 |
|---|---|---|---|
| 2 | 1축 위치·속도 | $10^{4}$ | 80 kB |
| 4 | 수평 위치·속도 | $10^{8}$ | 0.8 GB |
| 6 | 3축 위치·속도 | $10^{12}$ | 8 TB |
| 12 | 6자유도 강체 전체 | $10^{24}$ | 계산 불가 |
그래서 실무는 세 길로 간다. ① 제약마다 저차원으로 나눈다(수평 정지 거리, 수직 고도, 선회 반경을 따로). ② 해석적 상한을 사용한다(정지 거리·선회 반경처럼 손으로 푸는 식, 2.6.4.2). ③ 짧은 앞날만 온라인으로 계산한다. 어느 길이든 나눈 방식이 보수적인지를 따로 보여야 한다.
7.8.4.3 제어 장벽 함수 — 끊지 않고 깎는다
Simplex는 경계에서 끊고 넘긴다. 다른 방법은 복잡 기능의 명령을 필요한 만큼만 깎는 것이다. 제어 장벽 함수(CBF, control barrier function)는 안전한 상태에서 0 이상인 함수 $h(\mathbf x)$를 두고, $h$가 줄어드는 속도를 제한한다(Ames 외, 2017).
$$\dot h(\mathbf x,\mathbf u)\ \ge\ -\alpha\,h(\mathbf x)$$
$h$가 크면(경계에서 멀면) 거의 아무 명령이나 허용하고, $h$가 0에 가까우면 $h$를 줄이는 명령을 막는다. 매 주기 이 부등식을 제약으로 두고 복잡 기능의 명령과 가장 가까운 명령을 2차 계획법으로 고르는 것이 안전 필터다. 1차원 접근에서 $h=d-d_{\min}-v^{2}/(2a)-vT$로 두면, 벽 쪽 가속도 $u$의 상한이 식 하나로 나온다.
$$u\ \le\ \frac{\alpha h-v}{v/a+T}$$
$a=4$ m/s², $T=0.23$ s, $\alpha=2$ /s, $d_{\min}=1$ m, $v=8$ m/s로 계산했다.
| 벽까지 $d$ | $h$ | 허용 가속도 상한 | 뜻 |
|---|---|---|---|
| 20 m | 9.19 m | +4.66 m/s² | 제한 없음(최대 가속 4보다 크다) |
| 14 m | 3.19 m | −0.73 m/s² | 가볍게 감속해야 한다 |
| 12 m | 1.19 m | −2.53 m/s² | 강하게 감속 |
| 11 m | 0.19 m | −3.43 m/s² | 거의 최대 감속 |
필터는 명령을 매끄럽게 바꿔 승차감과 임무 성능에 유리하다. 대가가 둘이다. 필터가 안전 경로 안에 들어와 그 자체가 높은 보증 대상이 되고, 모형($a$, $T$)이 틀리면 보장이 사라진다. 연속 시간 이론에는 지연이 없으므로 $T$를 $h$에 넣어 조여야 한다. 학습 기반 제어기에 안전 필터를 씌우는 방식은 7.7이 이어 작성한다.
같은 제약을 최적화 안에서 미리 보는 모델 예측 제어와의 비교는 2.15.8이 다룬다.
7.8.5 전환 시간 예산 — 감시·전환·복구 기동
결론부터: 경계의 폭은 지연 합 × 속도 + 회복 기동 거리 + 위치 오차다. 지연 몫은 속도에 비례하고 회복 기동 몫은 속도의 제곱에 비례한다. 식의 꼴은 2.6.4.2의 완충 폭, 2.14.5.1의 필요 탐지 거리와 같다.
$$d_{\text{경계}}=v\,(t_m+t_s+t_r)+d_{\text{회복}}(v)+e_{\text{위치}},\qquad d_{\text{회복}}=\frac{v^{2}}{2a}\ (\text{멀티콥터}),\quad \frac{v^{2}}{g\tan\phi}\ (\text{고정익 선회})$$
| 기호 | 뜻 |
|---|---|
| $t_m$ | 감시 지연 — 측정·전달, 판정 확인(연속 표본) |
| $t_s$ | 전환 지연 — 권한 이양, 적분기·설정값 초기화(2.10.8.1의 ④) |
| $t_r$ | 복구 기동 지연 — 작동기·자세가 회복 명령에 응답하기까지 |
| $a$, $\phi$ | 회복 기동의 감속도, 고정익의 선회 경사각 |
2 kg 쿼드콥터의 제어 수준 RTA(감시기가 50 Hz로 위치·속도를 본다) 예산을 2.2의 기준 설계에서 잡았다.
| 항목 | 값 | 근거 |
|---|---|---|
| 거리계 표본·전달 | 0.02 s | 50 Hz 위치·속도 루프(2.2.5) |
| 연속 2표본 확인 | 0.02 s | 오경보를 줄이는 연속 판정(2.5.5.3의 논리) |
| 권한 이양 | 0.02 s | 한 주기 |
| 감속 응답 | 0.167 s | 자세 이득 6 /s의 시정수(2.2.3) |
| 합계 $T$ | 0.227 s | 감속 4 m/s²(기울기 22°, 2.6.4.2) |
같은 식에 다른 수준의 지연을 넣으면 경계가 크게 달라진다(감속 4 m/s², 위치 오차 제외).
| RTA의 수준 | 지연 합 $T$ | 5 m/s | 10 m/s | 15 m/s | 10 m/s에서 지연 몫 |
|---|---|---|---|---|---|
| 제어 수준(기체 안 감시기) | 0.23 s | 4.3 m | 14.8 m | 31.5 m | 15 % |
| 지오펜스 수준(2.6.4.2의 판정·지령) | 1.0 s | 8.1 m | 22.5 m | 43.1 m | 44 % |
| 사람이 회복(링크 1 s + 인지·결정 5 s, 2.14.3) | 6.0 s | 33.1 m | 72.5 m | 118.1 m | 83 % |
| 제어 수준, 추력 여유가 적은 기체(감속 2 m/s²) | 0.23 s | 7.4 m | 27.3 m | 59.6 m | 8 % |
사람을 회복 기능으로 두면 10 m/s에서 경계가 다섯 배 가까이 넓어진다. 그 대부분이 지연 몫이다. 사람이 여러 대를 감독할 때 이 지연은 더 길어진다(7.11). 고정익 계열도 계산했다. 6 kg 결합형이 순항 13.9 m/s에서 30° 선회로 벗어나는 거리는 34.1 m이고, 지연 0.23 s를 더하면 37.3 m, 1.0 s면 48.0 m다(위치 오차 3 m를 더한 2.6.4.2의 51 m와 맞는다).
경계를 정했으면 인지가 그보다 멀리 봐야 한다. 장애물을 알아채는 거리가 경계 폭에 인지 지연 동안의 이동을 더한 것보다 짧으면 감시기는 판정할 재료가 없다. 장애물 일반의 필요 탐지 거리는 7.1, 공중 충돌은 2.14.5가 같은 논리로 다룬다.
7.8.6 Simplex 전환 시뮬레이션 — 1차원 접근 과제
7.8.6.1 모형
2 kg 쿼드콥터가 교량 벽면에 다가가 벽에서 2.0 m에 멈춰 점검한다. 안전 제약은 벽에서 1.0 m 안으로 들어가지 않는다이다. 아래 가정은 모두 교육용이다.
| 항목 | 값(가정) |
|---|---|
| 시작 거리·접근 속도 | 25 m, 6~10 m/s(균등 분포) |
| 기체 응답 | 가속 명령에 1차 지연 0.167 s, 최대 감속 4 m/s², 50 Hz |
| 복잡 기능 | 영상 거리 추정(지연 0.1 s, 잡음 0.3 m)으로 자기 지연을 내다보며 감속 2.5 m/s² 윤곽을 따른다 |
| 복잡 기능의 오류 | 거리를 3~10 m 멀게 읽는 인지 오류(얇은 구조물·유리면, 7.1) |
| 안전 감시기 | 독립 거리계(지연 1표본, 잡음 0.10 m)와 속도 추정(지연 0.1 s), 여유 0.2 m, 연속 2표본이면 전환 |
| 회복 기능 | 최대 감속 4 m/s²로 정지 후 유지 |
| 공통 원인 | 감시기의 거리계도 같은 오류를 낸다 |
| 반복 | 조건마다 3,000회(그림은 점마다 1,500회), 고정 시드 |
설계 변수는 감시기가 경계에 넣은 지연 버짓 $T_b$다. 실제 지연 합은 앞 절의 0.227 s다.
7.8.6.2 결과
RTA가 없으면 복잡 기능의 오류는 매번 제약을 침범한다(3,000회 중 3,000회). 오류가 없을 때는 평균 4.88 s에 점검 위치에 닿고 가장 가까이 간 거리는 1.66 m로 제약을 만족한다.
| 지연 버짓 $T_b$ | 침범(오류, 독립 감시기) | 침범(오류, 공통 원인) | 전환(정상 비행) | 정상 비행의 점검 위치 도달 |
|---|---|---|---|---|
| 0 s | 0.873 | 1.000 | 0.000 | 1.000 |
| 0.20 s | 0.066 | 1.000 | 0.000 | 1.000 |
| 0.25 s | 0(3,000회 중) | 1.000 | 0.000 | 1.000 |
| 0.30 s | 0 | 1.000 | 0.040 | 0.960 |
| 0.35 s | 0 | 1.000 | 0.406 | 0.594 |
| 0.50 s | 0 | 0.912 | 1.000 | 0.000 |
| 1.00 s | 0 | 0.479 | 1.000 | 0.000 |
읽을 것이 넷이다. 첫째, 버짓이 실제 지연보다 작으면 RTA가 있어도 막지 못한다. 0.03 s를 덜 넣은 0.20 s에서 오류의 6.6 %가 침범한다. 둘째, 버짓을 넉넉히 잡으면 정상 비행을 끊는다. 0.35 s에서 정상 접근의 41 %가 회복 기능으로 넘어가 점검 위치에 닿지 못한다. 사용할 수 있는 창은 0.25~0.30 s로 좁다. 셋째, 공통 원인은 버짓으로 풀리지 않는다. 감시기가 같은 오류로 속으면 1.0 s의 넓은 경계도 절반만 막고, 그때는 정상 비행을 모두 끊는다. 넷째, 3,000회 무침범은 $q$가 0이라는 뜻이 아니다. 95 % 신뢰로 말할 수 있는 상한은 약 $3/3000=1.0\times10^{-3}$이다(1.16.7).
7.8.6.3 복잡 기능의 성능과 감시기의 경계
복잡 기능을 더 공격적으로 만들면(늦게·강하게 감속) 무엇이 일어나는지 같은 버짓 0.25 s에서 계산했다(조건마다 1,500회).
| 복잡 기능의 감속 윤곽 | RTA 없을 때 도착 시간 | RTA 있을 때 정상 비행의 전환 | 점검 위치 도달 |
|---|---|---|---|
| 2.0 m/s² | 5.12 s | 0.000 | 1.000 |
| 2.5 m/s²(기준) | 4.88 s | 0.000 | 1.000 |
| 3.0 m/s² | 4.61 s | 0.999 | 0.001 |
| 3.5 m/s² | 3.50 s | 1.000 | 0.000 |
감속을 2.5에서 3.0 m/s²로 올려 얻는 이득은 0.27 s(5.5 %)인데, 그 대가로 거의 모든 접근을 감시기가 끊는다. 복잡 기능의 정상 궤적이 전환 경계 안으로 들어오기 때문이다. 결론은 분명하다. 복잡 기능은 감시기의 경계를 알고 그 바깥에서 성능을 짜야 한다. 학습 기반 기능이라면 경계를 학습의 제약이나 보상에 넣는다. RTA는 위험을 막지만 성능의 상한도 정한다. 이 시뮬레이션은 1차원 장난감 모형이며 바람·센서 탈락·다차원 기동을 넣지 않았다.
7.8.7 정형 검증 — 무엇을 증명할 수 있고 무엇은 못 하는가
7.8.7.1 네 가지 방법
정형 검증은 시스템의 모형이나 코드에 대해 "모든 경우에" 성질이 성립함을 수학으로 보인다. 시험이 고른 점을 확인한다면 증명은 집합 전체를 포괄한다. 항공 소프트웨어 보증에서는 RTCA DO-333(DO-178C의 정형 기법 보충서)이 정형 기법을 일부 시험·검토의 대체 수단으로 사용하는 조건을 정한다(8.8).
| 방법 | 하는 일 | 증명할 수 있는 것(예) | 한계 | 항공 사례 |
|---|---|---|---|---|
| 모형 검사(model checking) | 유한 상태 모형의 모든 경로를 기계적으로 탐색 | 비행 모드 논리에서 두 명령원이 동시에 권한을 갖지 않는다, 전환 뒤 반드시 회복 모드에 머문다 | 상태 폭발, 연속 동역학은 추상화가 필요 | 모드 논리·전환기 검증 |
| 정리 증명(theorem proving) | 사람이 세운 증명을 기계가 한 단계씩 검사 | 연속 동역학을 포함한 불변 성질(경계 안이면 회복 뒤에도 안전) | 전문가의 노동, 모형과 코드 사이의 간극 | ACAS X 권고의 안전 영역 증명(Jeannin 외, 2015) |
| 추상 해석(abstract interpretation) | 코드의 모든 실행을 포괄하는 근사 집합을 계산 | 0으로 나누기·넘침·배열 범위 같은 런타임 오류가 없다 | 기능이 옳다는 증명은 아니다. 근사 때문에 오경보 | Astrée가 에어버스 A340의 1차 비행 제어 소프트웨어(C 약 13만 줄)에서 런타임 오류 부재를 보였다(2003) |
| 런타임 검증(runtime verification) | 실행 중에 사양 위반을 감시 | 이번 실행에서 위반이 있었는가 | 미래를 보장하지 않는다 | RTA의 안전 감시기 |
Jeannin 외(2015)는 하이브리드 시스템 정리 증명으로 ACAS X 권고가 안전한 기하 조건을 보였고, 그 과정에서 당시 판의 권고가 안전 정리와 어긋나는 경우를 찾아냈다. 증명이 설계 결함을 찾는 도구이기도 하다는 사례다.
7.8.7.2 증명이 말하지 않는 것
증명은 모형과 가정에 대한 것이다. 세 간극이 남는다.
- 모형과 실물의 간극. 증명은 "감속 4 m/s²"를 가정하지만 실제 기체는 배터리 전압·바람·프로펠러 손상에 따라 감속이 바뀐다.
- 사양의 옳음. 증명은 사양을 만족함을 보일 뿐 사양이 옳은지는 말하지 않는다. "벽에서 1 m"가 실제로 충분한지는 안전성 평가가 정한다(8.4).
- 환경과 센서의 가정. 증명은 측정 오차가 $e$ 이하라고 가정한다. 유리면에서 거리계가 10 m 틀리면 가정이 깨진다.
그래서 정형 검증과 RTA는 짝을 이룬다. 증명에 사용한 가정 자체를 운용 중에 감시하면(지연이 $T$ 이하인가, 측정 잔차가 문턱 안인가, 상태가 ODD 안인가) 간극의 일부를 런타임으로 보완한다. 이를 가정-보장(assume-guarantee) 구조라 부른다. 항법 무결성 감시(4.4.5.4)도 같은 역할을 한다.
7.8.7.3 RTA를 증명하는 작은 정리
1차원 접근의 감시기는 손으로 증명할 수 있을 만큼 작다. 다음 네 가정이 성립한다고 하자. ① 감시기의 거리·속도 오차가 $e_d$, $e_v$ 이하다. ② 판정에서 회복 감속이 완전히 걸리기까지 지연이 $T$ 이하다(표본 간격 포함). ③ 지연이 지난 뒤 회복 기능은 감속 $a$ 이상을 낸다. ④ 지연 동안 복잡 기능의 가속은 $a_{+}$ 이하다. 감시기가 측정값 $\hat d$, $\hat v$로 다음을 만족하는 첫 표본에서 넘기면, 기체는 $d\ge d_{\min}$을 만족한다.
$$\hat d-d_{\min}\ \le\ \bar v\,T+\tfrac12 a_{+}T^{2}+\frac{(\bar v+a_{+}T)^{2}}{2a}+e_d,\qquad \bar v=\hat v+e_v$$
증명의 줄기는 짧다. 넘기기 직전 표본에서는 부등식이 성립하지 않았으므로 실제 거리가 우변보다 크다. 지연 동안 기체가 가는 거리는 $\bar vT+\tfrac12a_{+}T^{2}$ 이하이고, 그 끝의 속도 $\bar v+a_{+}T$에서 감속 $a$로 멈추는 거리가 마지막 항이다. 셋의 합이 남은 거리보다 작으니 제약에 닿지 않는다. 이 정리에서 읽을 것은 증명의 가정 네 개가 곧 감시하고 시험해야 할 목록이라는 점이다. ②는 최악 실행 시간 분석(2.10), ③은 비행 시험(8.20), ①은 센서 특성화, ④는 복잡 기능의 출력 제한으로 입증한다.
7.8.8 신경망 검증의 현황과 한계
신경망 검증은 "입력이 이 영역 안에 있으면 출력이 이 성질을 만족한다"를 증명한다. 두 종류의 성질이 흔하다. 입출력 성질(예: 침입기가 오른쪽 가까이에 있으면 "왼쪽 강하게 선회"를 권고하지 않는다)과 국소 강건성(입력을 $\epsilon$ 안에서 섭동시켜도 분류가 바뀌지 않는다)이다.
방법은 두 갈래다. 완전한 방법은 성질이 거짓이면 반드시 반례를 찾는다. SMT 기반의 Reluplex(Katz 외, 2017)와 그 후속 Marabou(2019), 혼합 정수 계획법이 이쪽이다. 불완전한 방법은 출력의 범위를 위아래로 묶어 빠르지만 "모르겠다"를 낼 수 있다. 구간 전파·추상 해석(DeepPoly 등)·선형 완화 기반 경계 전파(CROWN 계열)가 이쪽이고, 최근 도구는 둘을 분기 한정으로 섞는다. 2020년부터 열리는 신경망 검증 경진대회(VNN-COMP)가 도구의 발전을 비교한다.
규모의 벽을 숫자로 보자.
| 대상 | 크기 | 뜻 |
|---|---|---|
| ACAS Xu 압축 신경망 하나(Katz 외의 시험 대상) | 입력 5, 은닉층 6개 × ReLU 50개 = 300개 | ReLU 켜짐·꺼짐 조합의 상한 $2^{300}\approx2.0\times10^{90}$ |
| 같은 입력을 축마다 100점으로 시험 | $10^{10}$점 | 점 사이는 여전히 포괄하지 못한다 |
| 224×224 컬러 영상을 받는 인지망 | 입력 150,528차원 | 국소 강건성 정도만 현실적으로 다룬다 |
Reluplex는 300개 뉴런의 ACAS Xu 망에서 일부 안전 성질을 증명하거나 반례를 찾았다. 조합을 다 세지 않고 가지치기로 푸는 것이 핵심이다. 그러나 이 성공을 인지 신경망으로 옮기기는 어렵다. 한계는 다섯이다.
- 사양의 벽. "영상에 전선이 있으면 탐지한다"를 입력 픽셀의 수식으로 나타낼 수 없다. 증명할 사양이 없으면 검증할 수 없다.
- 국소 강건성은 세상에서의 옳음이 아니다. 어떤 영상 둘레 $\epsilon$ 안에서 안정하다는 것은 다른 날씨·다른 장소의 영상에 대해 말하지 않는다(분포 이동, 7.4).
- 규모. 인지망 크기의 완전한 검증은 아직 현실적이지 않다
(2026년 중반 문헌 기준, 도구 발전이 빠르다). - 검증한 망과 탑재한 망의 차이. 양자화·부동소수점·컴파일이 망을 바꾼다. 증명은 탑재 형태에 대해 다시 해야 한다.
- 재학습이 증명을 지운다. 망을 고치면 증명도 다시 한다. 형상 관리(8.22)의 대상이다.
실무의 결론은 이렇다. 작은 결정·제어 신경망(ACAS Xu형)은 검증하고, 인지 신경망은 분포 밖 입력 탐지와 불확실성 교정(7.4)으로 거르며 RTA로 감싼다. 2.14의 연구 질문(학습 기반 회피 로직의 증거)이 이 결론 위에 있다.
7.8.9 수치 예시·워크스루 — 교량 점검 쿼드의 RTA 설계
과제. 2 kg 쿼드콥터가 영상 기반 학습 제어기(복잡 기능)로 교량 벽면에 다가가 2.0 m에서 점검한다. 사람 위 운용은 없고, 운용 위험 평가에서 RTA를 완화 수단으로 제시하려 한다(17.17). 앞 절의 모형과 값을 사용한다.
- 제약과 ODD. 제약은 "벽에서 1.0 m 이상"이다. 운용 설계 영역(ODD)은 접근 속도 10 m/s 이하, 회복 기능이 호버를 유지할 수 있는 풍속 이하로 둔다. 감속 4 m/s²를 낼 추력 여유가 그 바람에서도 남는지를 확인한다.
- 회복 기능. 최대 감속으로 정지하고 유지한다. 단순한 상태 되먹임이라 증명과 시험이 쉽다.
- 지연 버짓과 경계. 실제 지연 합 0.227 s에 표본 간격 여유를 더해 $T_b=0.25$ s로 정한다. 10 m/s에서 경계는 제약 앞 15.2 m(여유 0.2 m 포함)다.
- 감시기의 센서. 복잡 기능은 카메라를, 감시기는 독립 거리계를 사용한다. 유리면과 얇은 구조물은 두 센서를 함께 속일 수 있으므로 $\beta$를 0.05로 보수적으로 가정한다. 줄이려면 원리가 다른 센서를 하나 더 달거나 해당 표면을 ODD에서 뺀다.
- 경계의 입증. 고장 주입 3,000회에서 침범 0이면 $q\le1.0\times10^{-3}$(95 %)를 말할 수 있다. 7.8.7.3의 정리로 경계식의 옳음을, 최악 실행 시간 측정으로 가정 ②를 입증한다.
- 잔여 위험. 복잡 기능이 접근 1회에 위험한 명령을 낼 확률을 $p=10^{-2}$(가정)로 두면 접근 1회당 침범 확률은 다음과 같다.
| $p$ | RTA 없음 | $\beta=0$ | $\beta=0.01$ | $\beta=0.05$ |
|---|---|---|---|---|
| $10^{-1}$ | $1.0\times10^{-1}$ | $1.0\times10^{-4}$ | $1.1\times10^{-3}$ | $5.1\times10^{-3}$ |
| $10^{-2}$ | $1.0\times10^{-2}$ | $1.0\times10^{-5}$ | $1.1\times10^{-4}$ | $5.1\times10^{-4}$ |
| $10^{-3}$ | $1.0\times10^{-3}$ | $1.0\times10^{-6}$ | $1.1\times10^{-5}$ | $5.1\times10^{-5}$ |
$\beta=0.05$이면 RTA의 이득은 20배에 그친다. 독립 감시기의 성능($q$)을 열 배 좋게 해도 거의 변하지 않는다. 이 설계의 투자처는 감시기의 정밀도가 아니라 독립성이다.
- 정상 운용의 비용. 기준 복잡 기능은 정상 비행에서 한 번도 끊기지 않는다. 그러나 개발팀이 접근 시간을 5.5 % 줄이려고 감속 윤곽을 3.0 m/s²로 올리면 거의 모든 접근이 끊긴다(7.8.6.3). 복잡 기능과 경계는 함께 형상 관리해야 한다(8.22).
- 증거 묶음. 경계의 정리, 지연의 측정, 고장 주입 결과, 공통 원인 분석(8.4), 전환 사건의 비행 기록(8.23)을 묶어 안전 사례로 낸다(8.7).
결론: 이 RTA의 성패는 감시기의 판정 정밀도보다 지연 버짓의 정확성과 센서의 독립성에서 결정된다. 복잡 기능의 성능 개선은 경계와 함께 다시 입증해야 한다.
7.8.10 설계 트레이드오프 — 끊을 것인가, 깎을 것인가, 증명할 것인가
① Simplex 전환(끊고 넘긴다). 감시기와 회복 기능이 단순해 증명과 인증 논증이 가장 쉽다. 대가는 전환 때의 급변과 보수적인 경계가 만드는 잦은 개입이다. 소형·중형 UAS의 오픈소스 스택을 감싸는 현실적인 길이다(2.10.11).
② 안전 필터(깎는다). 제어 장벽 함수로 명령을 연속으로 고친다. 임무 성능과 승차감이 좋다. 대가는 필터가 안전 경로 안에 들어와 그 자체를 높은 보증으로 만들어야 하고, 모형 오차에 민감하다는 점이다. 연구와 고성능 군용 기동에서 많이 사용된다.
③ 복잡 기능 자체를 증명한다. RTA 없이 작은 신경망이나 제어 법칙을 정형 검증한다. 개입이 없고 성능 손실이 없다. 대가는 검증할 수 있는 크기의 한계와 재학습마다 다시 하는 증명이다. ACAS Xu형 결정 로직처럼 입력이 저차원인 기능에 맞다.
견해: 인지가 들어가는 기능에는 ①을 기본으로 두고, 승객이 타거나 승차감이 중요한 AAM의 비행 제어에서는 ①의 바깥 경계 안쪽에 ②를 병용하는 편이 낫다고 본다. 근거는 셋이다. 첫째, 인지 신경망은 사양을 사용할 수 없어 ③이 불가능하다(7.8.8). 둘째, 이 장의 시뮬레이션처럼 경계는 좁은 창 안에서 정해야 하는데, ①은 그 창을 시험과 정리로 함께 입증하기 쉽다. 셋째, ②만 사용하면 필터의 모형이 틀린 순간 마지막 방어선이 없다. 바깥의 ①이 그 방어선이다. 반대 입장도 있다. 개입이 잦은 ①은 운용자의 신뢰를 깎고 불필요한 비상 착륙을 늘려 그 자체가 위험이 된다는 주장이다(2.6.9). 이 판단은 공개된 인증 사례가 거의 없는 상태의 해석이다.
7.8.11 세 축 비교
| 항목 | 군용 드론 | 민간 UAS | AAM |
|---|---|---|---|
| 감싸는 대상 | 학습 기반 임무 자율, 고기동 비행(운용 개념 수준) | 오픈소스 오토파일럿, 영상 기반 회피·착륙 | 학습 기반 비행 보조, 단계적 자율 비행 |
| 회복 기능 | 비행 영역 보호·지면 충돌 회피(Auto-GCAS의 개념)·귀환 | 정지·귀환·비상 착륙·낙하산(2.6) | 검증된 기본 제어 법칙, 대체 착륙(2.3) |
| 사람의 자리 | 운용자가 감독, 링크 없이도 도는 회복이 필요 | 원격 조종사가 회복 기능인 경우가 흔하다(지연 초 단위) | 조종사·원격 운항자가 감독(7.11) |
| 정형 검증의 용도 | 군 감항 증거의 일부(12.3) | 거의 사용하지 않음, 시험 기반 | 모드 논리·비행 제어 코드(DO-333) |
| 핵심 난제 | 링크 없는 감시, 전술 환경의 ODD | 낮은 비용의 독립 센서, SORA에서의 인정 | 승객 안전 수준의 공통 원인 입증 |
| 이어지는 장 | 10.9·12.3 | 2.10·17.17 | 15.23·20.10 |
7.8.12 관련 규격·프로토콜
| 문서 | 발행 | 무엇을 정하나 | 상세 |
|---|---|---|---|
| ASTM F3269-21 | ASTM(F38) | RTA로 복잡 기능을 가진 항공기 체계의 거동을 한정하는 방법(입력 관리·감시기·전환기·회복 기능, 사건 시간) | 이 장·8.8 |
| ASTM F3201-26 | ASTM(F38) | UAS 소프트웨어의 신뢰성 확보 관행(2026년 판이 현행, 판매 페이지 기준) | 8.8 |
| RTCA DO-178C / EUROCAE ED-12C | RTCA·EUROCAE | 소프트웨어 개발 보증 | 8.8·20.9 |
| RTCA DO-333 / EUROCAE ED-216 | RTCA·EUROCAE | 정형 기법 보충서(DO-178C·DO-278A) (ED 번호 확인 필요) | 8.8 |
| SAE ARP4754B · ARP4761A | SAE | 개발 보증 수준의 배정과 독립성, 안전성 평가 | 8.2·8.4 |
| IEC 61508-6 | IEC | 공통 원인 $\beta$-요인 모형 | 2.5 |
| RTCA DO-386 / EUROCAE ED-275 | RTCA·EUROCAE | ACAS Xu 최소 운용 성능 (2차 확인, 확인 필요) | 9.13 |
| EASA AI 개념서 Issue 02(2024), NPA 2025-07 | EASA | 학습 보증·설명 가능성·인간-AI 협업 지침, AI 신뢰성 규칙 제정 첫 단계(RMT.0742) | 20.10 |
유료 표준(ASTM·RTCA·SAE)의 본문은 옮기지 않고 공개 요약의 범위에서 작성했다. 규격의 지형은 A.6가 모은다.
7.8.13 관련 규제·인증 요구와의 연결
| 요구 | RTA·정형 검증과의 연결 | 상세 |
|---|---|---|
| 인증기준 합의 | RTA를 적합성 입증 수단으로 사용하려면 특별조건·이슈페이퍼로 기준을 합의한다 | 20.5·20.6 |
| 개발 보증 수준 배분 | 감시기·회복 기능에 높은 수준, 복잡 기능은 독립성 논증으로 조정 | 8.4·8.8·20.9 |
| 운용 위험 평가 | RTA를 지상·공중 위험의 완화 수단으로 제시, 강건성 수준의 증거 | 17.17·20.14 |
| AI 규율 | 학습 보증과 인간 감독 의무, 고영향 AI의 기록·설명 (적용 범위 확인 필요) | 18.21·20.10 |
| 군 감항 | 학습 기반 기능을 포함한 체계의 감항 증거 | 12.3·20.19 |
| 변경 관리 | 경계 파라미터·지연 버짓·복잡 기능의 판을 함께 형상 관리 | 8.22·20.23 |
| 사고 조사 | 전환 사건과 감시기 판정을 기록해 사후 설명 가능하게 | 8.23 |
7.8.14 함정과 한계
| 오해 | 실제 | 더 볼 곳 |
|---|---|---|
| "감시기가 있으니 복잡 기능은 아무거나 사용해도 된다" | 정상 궤적이 경계 안으로 들어오면 매번 끊긴다. 복잡 기능은 경계를 알고 설계해야 한다 | 7.8.6.3 |
| "경계는 정지 거리면 된다" | 지연 몫이 빠지면 RTA가 있어도 침범한다. 0.03 s 부족이 6.6 % | 7.8.5·7.8.6.2 |
| "감시기를 더 정밀하게 하면 된다" | 공통 원인이 하한을 정한다. 독립성이 먼저다 | 7.8.3.3·1.16.7.1 |
| "사람이 감시하면 가장 안전하다" | 사람이 회복 기능이면 경계가 다섯 배 넓어진다 | 7.8.5·7.11 |
| "증명했으니 안전하다" | 증명은 모형·사양·가정에 대한 것이다. 가정을 운용 중에 감시해야 한다 | 7.8.7.2 |
| "신경망도 검증하면 된다" | 인지망은 사양을 사용할 수 없고 규모가 크다. 작은 결정망만 현실적이다 | 7.8.8 |
| "3,000회 무사고면 실패 확률 0" | 95 % 상한이 $10^{-3}$일 뿐이다 | 7.8.6.2·1.16.7 |
이 장의 한계도 밝혀 둔다.
- 시뮬레이션은 1차원 장난감 모형이다. 바람·센서 탈락·측면 기동·여러 장애물을 넣지 않았고, 복잡 기능의 오류는 거리 바이어스 한 종류다.
- 지연 버짓은 2.2의 기준 설계에서 빌린 가정이다. 실제 기체는 최악 실행 시간과 응답을 측정해 정한다.
- ASTM F3269의 요건은 공개 요약 수준이다. 표준의 세부 요구(커버리지 분석·사건 시간 요건)는 원문으로 확인해야 한다.
- 인증 쪽 상태는 빠르게 바뀐다. RTA로 개발 보증 수준을 얼마나 조정할 수 있는지는 공개된 일반 규칙이 없고 사례별이다
(확인 필요).
7.8.15 체크포인트·연구 질문
체크포인트
- RTA의 다섯 구성 요소를 적고, 이 가운데 높은 보증 수준이 필요한 것과 그 이유를 말하라.
- 감속 4 m/s², 지연 합 0.5 s인 기체가 8 m/s로 접근할 때 전환 경계의 폭을 구하라. 지연 동안 복잡 기능이 4 m/s²로 가속하는 최악을 가정하면 얼마나 늘어나는가?
- 허용 집합·회복 가능 집합·전환 경계의 관계를 그림으로 설명하라.
- Simplex 전환과 제어 장벽 함수 안전 필터의 장단점을 각각 둘씩 말하라.
- 복잡 기능의 오류 확률 $10^{-2}$, 감시기 미탐지 $10^{-3}$, $\beta=0.01$일 때 잔여 위험을 구하고, 감시기를 열 배 좋게 했을 때의 변화를 말하라.
- 신경망 검증이 ACAS Xu형 망에서는 되고 인지 신경망에서는 어려운 이유를 사양과 규모로 설명하라.
연구 질문 — 이 장에서 파생되는 열린 주제(25.7에 모은다)
- 전환 경계의 데이터 기반 조정 — 비행 기록에서 실제 지연과 감속 분포를 추정해 경계를 갱신하면서도 증명의 가정을 만족하는 방법은?
- 인지 RTA의 독립성 입증 — 카메라·LiDAR·레이더가 함께 속는 조건(유리·연기·얇은 전선)의 $\beta$를 실측으로 추정하는 시험 설계는 무엇이어야 하는가(7.1·8.19)?
- RTA의 개발 보증 수준 배분 기준 — 감시기의 독립성 증거로 복잡 기능의 보증 수준을 얼마나 조정할 수 있는지 공통 기준을 세울 수 있는가(8.4·20.10)?
- 탑재 형태의 신경망 검증 — 양자화된 망을 직접 검증하고, 재학습 뒤의 증명을 점진적으로 갱신하는 방법은?
1차 출처(이 장)
- Seto, D.; Krogh, B.; Sha, L.; Chutinan, A., "The Simplex Architecture for Safe On-Line Control System Upgrades," Proc. American Control Conference, 1998, pp. 3504–3508.
- Sha, L., "Using Simplicity to Control Complexity," IEEE Software 18(4), 2001.
- ASTM F3269-21, Standard Practice for Methods to Safely Bound Behavior of Aircraft Systems Containing Complex Functions Using Run-Time Assurance, ASTM International(공개 요약).
- Mitchell, I. M.; Bayen, A. M.; Tomlin, C. J., "A Time-Dependent Hamilton–Jacobi Formulation of Reachable Sets for Continuous Dynamic Games," IEEE Transactions on Automatic Control 50(7), 2005.
- Ames, A. D.; Xu, X.; Grizzle, J. W.; Tabuada, P., "Control Barrier Function Based Quadratic Programs for Safety Critical Systems," IEEE Transactions on Automatic Control 62(8), 2017.
- Jeannin, J.-B. et al., "A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System," TACAS 2015, LNCS 9035.
- Katz, G.; Barrett, C.; Dill, D.; Julian, K.; Kochenderfer, M., "Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks," CAV 2017.
- Cousot, P. et al., "The ASTRÉE Analyzer," ESOP 2005.
- Clarke, E. M.; Grumberg, O.; Peled, D., Model Checking, MIT Press, 1999.
- RTCA DO-333, Formal Methods Supplement to DO-178C and DO-278A, 2011.
출처를 찾고 판을 추적하는 방법은 0.9에서 다룬다.
다음 장: 7.9(군집 I: 알고리즘·분산 제어·통신 제약)은 한 대의 안전 경계를 여러 대의 협조로 넓힌다. 이 장의 경계가 장애물과 한 기체의 문제였다면, 군집에서는 이웃 기체가 서로의 경계가 되고 통신 지연이 지연 버짓에 들어온다.