Automated, Credible Autocoding of An Unmanned Aggressive Maneuvering Car Controller

기술 요약: 무인 공격적 기동 자동차 제어기의 자동화된 신뢰성 있는 오토코딩

문제 정의
본 논문은 완전히 비선형적인 동역학을 특징으로 하는 제어 시스템에 신뢰할 수 있는 오토코딩 프레임워크를 적용하는 과제를 다룬다. 저자들의 이전 연구는 선형 및 준비선형(피드백 내에 유계된 비선형성이 존재하는) 제어기를 위한 자동화된 프레임워크를 성공적으로 입증했으나, 해당 방법들은 리아푸노프 안정성 증명에서 유도된 이차 불변량(quadratic invariants)에 의존했다. 여기서 다루는 구체적인 문제는, 기존의 프로토타입 도구들이 처리할 수 없었던 비이차 불변량(non-quadratic invariant)을 생성하는 비이차 리아푸노비 함수를 사용하는 비선형 자동차 제어기의 오토코딩이다. 또한, 초월 함수(transcendental functions)의 존재와 생성된 코드의 런타임 오류(예: 오버플로) 부재를 보장해야 하는 필요성은 자동 검증에 있어 상당한 장애물이 된다.

방법론
저자들은 제어 이론적 증명을 활용하여 코드를 생성하고 고수준의 기능적 속성을 검증하는 기존의 "제어 의미론 기반 오토코딩" 프레ك워크를 확장한다. 방법론은 다음 단계들을 포함한다:

1. 프레임워크 확장: 저자들은 프로토타입의 데이터 흐름 주석 언어(Simulink 및 Gene-Auto 기반)를 새로운 주석 심볼로 확장할 것을 제안한다. 구체적으로, 다음을 도입한다:

   • 하부 언어로 표현 가능한 모든 논리식을 수용할 수 있는 일반화된 동기 관측기 블록(generalized synchronous observer block): 이는 관찰되는 속성의 구조에 대한 제한을 제거한다.
   • 비선형 상태 전이 시스템을 정의할 수 있는 일반화된 플랜트 블록(generalized plant block): 선형 상태 공간 모델에 국한되지 않는다.

2. 시스템 모델링: 본 연구의 사례 연구는 정상 상태 코너링 평형점 주위로 단일 트랙 자동차 모델을 안정화하도록 설계된 슬라이딩 모드 기반 비선형 자동차 제어기이다. 제어기 아키텍처는 두 개의 서브시스템으로 구성된다:

   • 선형 서브시스템: 선형화된 모델을 평형점으로 구동하는 LQR 제어기로, 이차 불변량에 의해 제어된다.
   • 슬라이딩 모드 서브시스템: 명령된 슬립(slip)과 일치하도록 바퀴의 각속도를 관리하며, 비이차 리아푸노프 함수로부터 유도된 비이차 불변량($z^T z \leq 1$)에 의해 제로된다.

3. 수동 주석 및 변환: 비이차 불변량의 완전 자동 분석에 대한 현재 프로토타입의 한계로 인해, 저자들은 이 과정을 수동으로 시연한다. 저자들은 선형화된 플랜트 모델과 보조 동역학을 Simulink 모델에 임베딩한다. 안정성 증명은 다음과 같은 주석으로 표현된다:

   • 선형 부분은 이차 불변량을 위해 기존의 타원체(ellipsoid) 블록을 사용한다.
   • 비선형 부분은 비이차 불변량을 표현하기 위해 새로운 일반화된 동기 관측기를 사용한다.
   • 출력물은 ACSL(ANSI/ISO C 명세 언어) 표준과 유사한 주석을 가진 Matlab 코드(대상 C 코드의 대리물로 사용됨)로 변환된다.

4. 검증 로직: 본 논문은 불변량이 코드로 어떻게 매핑되는지 상세히 설명한다. 선형 불변량은 아핀 변환(affine transformation) 기술을 사용하여 전파된다. 비이차 불변량의 경우, 저자들은 호어 논리(Hoare logic)의 공리적 규칙을 이용한 역방향 전파(backward propagation)를 채택한다. 저자들은 포화 연산자(saturation operators)의 존재로 인해 다항식이나 매끄러운 함수에 대한 단일 일반 결정 절차를 사용할 수 없으므로, 비선형 케이스의 전조건과 후조건 사이의 함의를 증명하기 위해서는 정리 증명기(theorem prover)가 필요하다고 언급한다.

주요 기여

• 주석 언어의 확장: 일반적인 서술어 및 동역학 시스템을 지원하기 위해 새로운 주석 블록(일반화된 관측기 및 플랜트)을 제안함으로써, 선형/이차 가정의 제약을 넘어선다.
• 비이차 시스템에 대한 시연: 기존 프로토타입에서 지원되지 않았던 시나리오인, 비이차 불변량을 가진 완전 비선형 제어기를 처리하는 방법을 수동으로 시연한다.
• 런타임 오류 보장: 비이차 불변량($z^T z \leq 1$)이 물리적 제약 조건이 알려진 경우 시스템 변수(예: 바퀴 각속도)에 대한 경계를 설정하여 런타임 오류의 부재를 입증하는 인증서 역할을 할 수 있음을 보여주는 이론적 유도를 제시한다.

결과
본 논문은 제어 의미론으로부터 유도된 전조건, 후조건 및 가정을 삽입한 자동차 제어기의 수동 주석 예시를 제시한다.

• 선형 루프의 경우, 시스템은 이차 불변량을 성공적으로 식별하고 코드를 통해 이를 전파한다.
• 비선형 루프의 경우, 시스템은 비이차 불변량을 조건으로 성공적으로 삽입한다.
• 저자들은 프레임워크가 주석이 달린 코드를 생성할 수는 있지만, 함수들의 복잡성(특히 포화 연산)으로 인해 $A \to B$ (여기서 $A$와 $B$는 불변량에 의해 정의된 집합)의 자동 검증은 아직 완전히 자동화되지 않았음을 보여준다. 현재 검증은 백엔드 분석기를 돕기 위해 사용자가 필요한 불변량 사실(invariant facts)을 직접 삽입하는 것에 의존한다.

의의 및 주장
본 논문은 이 작업이 일반적인 비선형 시스템으로 신뢰할 수 있는 오토코딩을 확장하기 위한 필수적인 단계임을 주장한다. 이 연구의 의의는 제어 이론적 증명으로부터 시스템 동작의 "인증서"(안정성)와 런타임 안전성(유계성)을 직접 담고 있는 코드를 생성할 수 있는 능력에 있다.

• 겸허한 주장: 저자들은 비선형 케이스에 대한 현재 구현이 완전히 자동화되어 있지 않다는 점을 명시적으로 밝힌다. 그들은 이 과정이 "대부분의 경우 완전히 자동화될 수 없으며" 사용자가 새로운 관측기 블록을 사용하여 안정성 증명을 수동으로 삽입해야 한다고 기술한다.
• 확장성: 본 논문은 포화 및 초월 연산에서 발생하는 비다항 함수를 처리하기 위한 정리 증명기의 필요성, 특히 문서화된 출력 코드의 자동 분석 및 검증이 직면한 확장성 문제를 인정하며 결론을 맺는다. 이 연구는 모든 비선형 제어기를 위한 완전히 실현된 자동화 도구라기보다는, 프레임워크의 확장 가능성에 대한 개념 증명(proof-of-concept) 역할을 한다.