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

코드 계약 (Code contracts)은 임베디드 시스템 내 안전 필수 (safety-critical) 소프트웨어의 기능적 요구사항 (functional requirements)을 명시하는 강력한 방법을 제공합니다. 예를 들어, ANSI/ISO C 명세 언어 (ACSL)를 사용하여 C 코드의 기능적 동작을 명시할 수 있으며, 이는 Frama-C 프레임워크의 Wp 플러그인에 의해 형식 검증 (formally verified)될 수 있습니다. 그러나 제어 흐름 (control flow) 및 데이터 흐름 (data flow)에 대한 제한과 같은 비기능적 요구사항 (non-functional requirements) 또한 임베디드 시스템의 안전을 위해 중요합니다. 하청업체, 주니어 개발자가 작성하거나 대규모 언어 모델 (large language models)에 의해 생성된 신뢰할 수 없는 코드는 Wp에 의해 검증될 수 있지만, 그럼에도 불구하고 안전하지 않은 함수를 호출하거나 초기화되지 않은 프로그램 변수를 사용할 수 있습니다. 이 문제를 해결하기 위해, 우리는 안전 필수 임베디드 시스템 내 C 코드의 비기능적 요구사항에 관한 일련의 일반적인 규칙들을 구축했습니다. 우리의 규칙은 MISRA-C와 같은 대중적인 C 규칙 세트와는 직교 (orthogonal)하며, 모듈 및 인터페이스를 통한 모듈 간의 상호작용에 집중합니다. 우리의 규칙을 점검할 수 있도록, 우리는 C 모듈을 위한 인터페이스 명세 계약 언어를 제안합니다. 우리는 우리의 규칙을 점검하는 체커 (checker)를 Frama-C 플러그인으로 구현하였으며, 이 플러그인은 C 모듈과 그 계약을 입력으로 받아 제어 흐름 및 데이터 흐름 속성을 점검하여, 예를 들어 모듈에 의해 허용된 함수만 호출되는지 등을 보장합니다. 우리는 신뢰할 수 없는 코드에 대한 모듈 계약 및 ACSL 계약의 명세와 검증을 가능하게 하기 위해 우리의 체커를 툴체인 (toolchain)에 통합했습니다. 우리는 Scania 트럭에 사용되는 소프트웨어를 활용한 안전 필수 C 코드에 대한 두 가지 사례 연구를 보고하며, 여기서 우리는 비정형 시스템 요구사항을 기반으로 모듈 계약 및 ACSL 함수 계약을 정의하고 우리의 툴체인을 사용하여 이를 검증했습니다.