기술 요약: CNC 프로그램의 물리적 충돌 검증을 위한 분리 논리

1. 문제 제기

전통적인 컴퓨터 수치 제어 (CNC) 가공의 안전성 검증은 기하학적 시뮬레이션과 쓸어낸 부피 (swept volume) 분석에 크게 의존합니다. 이러한 방법들은 명백한 G 코드 오류를 식별하는 데 효과적이지만, 다음과 같은 근본적인 한계를 겪습니다:

• 상징적 증명 부재: 이들은 결정론적이고 상징적인 안전 증명이 아닌 확률적 확신을 제공합니다.
• 계산 비용: 사양이나 G 코드가 변경될 때 특히 반복적인 테스트 주기를 요구합니다.
• 불확실성 처리: 계산 비용이 급증하지 않으면서 연속 운동학 변수, 비결정적 급속 위치 지정 경로, 기계적 변동성 (예: 서보 지연) 을 엄격하게 고려하는 데 어려움을 겪습니다.
• 확장성: 기존 방법들은 종종 복잡한 다축 환경 (예: 5 축 테이블 - 테이블 구성) 과 협력형 다공구 시스템으로 효율적으로 확장되지 못합니다.

본 논문은 CNC 가공에서의 물리적 충돌을 관리된 자원 모델 내의 논리적 모순으로 재정의함으로써, 확률적 시뮬레이션에 대한 결정론적 대안을 제시한다고 주장합니다.

2. 방법론

제안된 프레임워크는 연속 물리 운동학을 이산 형식 논리에서 분리하는 파서 - 증명기 핸드셰이크 (Parser-Prover Handshake) 아키텍처를 도입합니다. 이 접근법은 물리적 CNC 작업 공간을 공간 힙 (Spatial Heap) 으로 개념화하여, 물리적 점유를 관리된 논리적 자원으로 취급합니다.

2.1 아키텍처 분리

시스템은 두 도메인 간의 엄격한 경계를 통해 작동합니다:

1. 파서 (연속 도메인): 원시 G 코드, 공구 기하학, 안전 마진을 소비하는 가상 머신으로 작동합니다. 이는 부동 소수점 좌표, 이송 속도 등 연속 운동학 변수와 물리적 불확실성을 이산 정수 도메인 ($Z^3$) 으로 소진합니다. 이는 사용자 정의 안전 마진 ($\epsilon$) 으로 공구 부피를 확장하기 위해 민코프스키 합 (Minkowski sums) 을 활용하고, 선형 보간 (G01) 에 대한 이산 보크셀 경로와 급속 위치 지정 (G00) 에 대한 경계 상자를 생성하기 위해 Bresenham 의 3D 알고리즘을 사용합니다.
2. SL 증명기 (이산 도메인): 파서가 방출한 이산 공간 집합에 엄격하게 작동합니다. 이는 메모리 관리자로서 공간 힙 ($h$) 에 대해 분리 논리 (SL) 삼중항을 평가합니다. 증명기는 변수 저장소를 쿼리하지 않으며, 공간적 불연속성만을 검증합니다.

2.2 공간 힙 모델

물리적 작업 공간은 유한 부분 함수 $h: Z^3 \rightharpoonup \{Tool, Environment, Stock, Empty\}$에 매핑됩니다.

• 공간 데이터 레이스: 물리적 충돌은 두 개의 서로 다른 물리적 자원 (예: 공구와 환경) 이 동시에 동일한 이산 메모리 주소를 소유하려고 할 때 발생하는 "공간 데이터 레이스"로 재정의됩니다.
• 분리 결합 ($*$): 핵심 논리 연산자는 하위 명제가 메모리의 불연속 부분에 대해 성립함을 주장합니다. $R(C_1, \theta_1) * R(C_2, \theta_2)$가 평가될 때, $C_1 \cap C_2 = \emptyset$인 경우에만 만족 가능합니다. 비어 있지 않은 교집합은 논리를 만족 불가능하게 만들어 결정론적으로 오류를 신호합니다.

2.3 검증 파이프라인

검증 과정은 단방향 파이프라인을 따릅니다:

1. 입력: 원시 G 코드, 공구 마스크 기하학, 안전 마진 ($\epsilon$), 해상도 인자.
2. 이산화: 파서는 입력을 이산 공간 집합 ($V_{start}, V_{final}, V_{path}$) 으로 변환합니다.
3. 논리 추론: 증명기는 분리 논리 삼중항 $\{ \Sigma_0 \} \text{CSL} \{ \Sigma_{final} \}$을 평가합니다.
   • 전제 조건 ($\Sigma_0$): 공구, 환경, 재료, 빈 공간의 초기 불연속 소유권을 주장합니다.
   • 명령 (CSL): 힙 변이로서 이산 운동 (예: G00, G01) 을 나타냅니다.
   • 후제 조건 ($\Sigma_{final}$): 공구의 이동과 재료 제거 후 업데이트된 소유권을 주장합니다.

2.4 동시성 및 다축 확장

• 동시 분리 논리 (CSL): 다공구 또는 협력 환경의 경우, 공간 힙은 스레드 로컬 서브힙 ($h_{local}$) 과 공유 힙 ($h_{shared}$) 으로 분할됩니다. 물리적 인계는 임계 영역 (Critical Regions) (with Res do C) 을 사용하여 형식적 소유권 이전으로 검증되며, 동적 잠금 없이 상호 배타성을 보장합니다.
• 다축 운동학: 프레임워크는 절삭 공구와 회전 가능한 공작물을 두 개의 동시적이며 상호 가변적인 공간 스레드로 취급함으로써 5 축 작업으로 확장됩니다. 파서는 회전 행렬을 사용하여 재료의 회전 쓸어낸 부피와 공구의 선형 쓸어낸 부피를 사전 계산하여, 둘 다 이산 집합으로 증명기에 제시합니다. 이는 복잡한 삼각함수 운동학을 증명 엔진에서 추상화합니다.

3. 주요 기여

• 충돌의 형식적 재정의: 본 논문은 물리적 점유와 논리적 메모리 소유권 간의 형식적 대응 관계를 수립하여, 물리적 충돌을 논리적 "공간 데이터 레이스"로 재정의합니다.
• 파서 - 증명기 핸드셰이크: 연속 불확실성을 이산 정수 도메인으로 소진하는 새로운 아키텍처 경계로, 증명기가 일반 포인터 연산의 복잡성을 피하면서 분리 논리의 처리 가능한 부분 내에서 작동할 수 있게 합니다.
• 기하학적 안전 마진 통합: 방법론은 민코프스키 합을 통합하여 이산 논리 내에서 직접 형식적 안전 마진 ($\epsilon$) 을 제공하며, 실제 세계의 기계적 불확실성을 고려합니다.
• 고급 운동학으로의 확장성: 프레임워크는 공작물을 동적으로 가변적인 공간 자원으로 모델링하고 공유 작업 공간 검증을 위해 동시 분리 논리를 활용함으로써 다축 (예: 5 축) 및 동시 다공구 환경을 네이티브로 지원합니다.

4. 결과 및 검증

본 논문은 다음을 통해 방법론을 시연합니다:

• 결정론적 검증: 시스템은 분리 논리 삼중항의 만족 가능성을 증명함으로써 안전한 궤적을 성공적으로 검증합니다.
• 충돌 감지: 피치에 대한 급속 이송과 관련된 사례 연구에서, 시스템은 "공간 데이터 레이스"(주장된 메모리의 비어 있지 않은 교집합) 를 감지하고 물리적 실행 전에 결정론적으로 오류 상태로 전환합니다.
• 동시성 및 인계: 프레임워크는 불연속 공간에서 두 공구의 병렬 실행과 공유 자원의 안전한 순차적 인계를 검증하여, 분리 결합이 상호 배타성을 강제함을 증명합니다.
• 다축 검증: 이 접근법은 복잡한 회전 운동학을 이산 보크셀 집합으로 축소함으로써 5 축 작동을 성공적으로 검증하며, 공구와 재료 경로가 환경이나 서로와 교차하지 않음을 증명합니다.

5. 중요성 및 주장

본 논문은 이 접근법이 확률적 확신 대신 안전에 대한 상징적 증명을 제공하는 전통적인 기하학적 시뮬레이션에 대한 결정론적 대안을 제공한다고 주장합니다. 시뮬레이션을 보완하는 역할을 함으로써, 프레임워크는 다음과 같은 목표를 가집니다:

• 반복적 테스트 감소: G 코드나 사양이 변경될 때 필요한 테스트 주기를 최소화합니다.
• 자율 제조 가능: 충돌이 적은 자율 제조 시스템에 대한 수학적으로 견고한 기반을 제공합니다.
• 복잡성 분리: 연속 운동학의 계산 부하를 논리적 증명에서 분리하여 복잡한 산업 응용 분야에 대한 형식적 검증을 처리 가능하게 만듭니다.

저자들은 이 작업을 모든 시뮬레이션을 대체하는 것이 아니라, 상태 전이가 발생하기 전에 안전 전제 조건이 충족되도록 보장하는 엄격하고 확장 가능한 계층으로 위치시킵니다. 이는 적층 제조와 같은 다른 분야에서 사용되는 기계적 의미론을 반영합니다. 향후 작업은 레거시 버그를 격리하기 위한 "부정확성 분리 논리 (Incorrectness Separation Logic)"와 임베디드 컨트롤러로의 실시간 통합을 탐구할 것으로 명시되어 있습니다.