임베디드 자동차 C 코드의 비기능적 요구사항에 대한 계약 기반 검증

요약

임베디드 자동차 소프트웨어의 안전성을 위해 C 코드의 비기능적 요구사항을 검증하는 새로운 방법론을 제안합니다. ACSL과 Frama-C를 활용하여 제어 및 데이터 흐름을 점검하는 규칙과 체커를 개발하였으며, Scania 트럭 사례를 통해 실효성을 입증했습니다.

핵심 포인트

• 비기능적 요구사항을 위한 새로운 C 코드 계약 규칙 구축
• Frama-C 플러그인 기반의 제어 및 데이터 흐름 검증 체커 구현
• LLM 생성 코드 등 신뢰할 수 없는 코드의 안전성 보장
• Scania 트럭 소프트웨어를 활용한 실제 사례 연구 수행