하이브리드 시스템 속성의 런타임 인포스먼트 (Runtime Enforcement)

런타임 인포스먼트 (Runtime enforcement)는 불확실하고 동적인 환경에서 작동하는 자율 시스템 및 사이버 물리 시스템 (Cyber-physical systems)의 안전성을 보장하기 위한 유망한 접근 방식으로 부상했습니다. 전통적인 런타임 검증 (Runtime verification)과 달리, 런타임 인포스먼트는 실행 중에 능동적으로 개입하여 안전하지 않은 시스템 동작을 수정함으로써 속성 위반을 방지합니다. 기존의 인포스먼트 프레임워크는 주로 비시간적 (Untimed) 또는 이산 시간 (Discrete-time) 명세에 초점을 맞추고 있으며, 이벤트의 지연 또는 억제에 국한되는 경우가 많아 복잡한 연속 동역학 (Continuous dynamics)을 보이는 반응형 시스템 (Reactive systems)에는 부적합합니다. 본 논문에서는 안전 요구 사항을 하이브리드 오토마타 (Hybrid Automata, HA)를 사용하여 모델링하는 런타임 인포스먼트 프레임워크를 제안합니다. 이 프레임워크는 이산 이벤트 편집 (Discrete-event editing)과 연속 시간 모니터링 (Continuous-time monitoring)을 결합하여 임의의 시간 시점에서 이벤트의 억제 (Suppression), 지연 (Delay), 삽입 (Insertion)과 같은 인포스먼트 동작을 지원합니다. 환경 입력을 관찰하면 오토마타가 초기화되며, 런타임 도달 가능성 분석 (Runtime reachability analysis)을 사용하여 안전한 교정 동작을 합성합니다. 우리는 안전 하이브리드 오토마타에 대한 인포스먼트 문제를 공식적으로 정의하고, 인포스먼트 가능 조건 (Enforceability conditions)을 확립하며, 반응형 시스템을 위한 온라인 인포스먼트 알고리즘을 제시합니다. 적응형 크루즈 컨트롤 (Adaptive Cruise Control, ACC) 시스템에 대한 상세한 사례 연구는 안전하지 않은 컨트롤러 동작 하에서도 안전 속성을 유지하는 데 있어 제안된 접근 방식의 효과를 입증합니다. 실험 결과는 이 프레임워크가 실시간으로 안전 요구 사항에 대한 지속적인 준수를 보장하면서도 계산 오버헤드 (Computational overhead)를 최소화함을 보여줍니다.