UPPAAL을 사용한 CAN 데이터베이스 검증 프레임워크

국문 초록 (Abstract)

세계적으로 가장 많이 사용되는 차량 내 네트워크인 CAN 네트워크에서는 여러 개의 제어기가 하나의 버스를 공유하기 때문에, 메시지 응답 시간의 지연이 불가피하다. 자동차는 대표적인 안전 필수 시스템 중 하나로, CAN 네트워크에서의 메시지 응답 시간이 지연되어 마감 시간을 초과하는 경우 운전자와 차량 전체의 안전성이 훼손될 수 있다. 그러므로 운전자 및 차량의 안전과 관련된 메시지는 응답 시간의 지연이 최소화되어야 하며, 메시지의 응답 시간이 마감 시간을 초과하지 않는지 CAN 데이터베이스를 사전에 검증하는 작업이 반드시 필요하다.
본 논문에서는 차량 내 네트워크의 종단 간 메시지 응답 시간 보장에 대한 첫 번째 연구로써, CAN 네트워크에서의 메시지 응답 시간의 보장을 검증한다. 이를 위하여, 정형 명세 및 검증 도구인 UPPAAL과 CAN 데이터베이스로부터 UPPAAL 모델을 자동 생성하는 DBC2XML 컴포넌트로 구성된 프레임워크를 제안한다.

목차 (Table of Contents)

• 제 1 장 서론
• 1.1 연구 배경
• 1.2 관련 연구
• 1.3 연구 목표
• 제 2 장 CAN 데이터베이스 검증 프레임워크
• 2.1 CAN 데이터베이스
• 2.2 DBC2XML
• 2.3 UPPAAL
• 2.3.1 모델링
• 2.3.2 시뮬레이션
• 2.3.3 검증
• 2.3.4 문법과 쿼리
• 제 3 장 모델 체킹을 사용한 검증
• 3.1 모델의 논리적인 속성 검증
• 3.2 모델의 시간적인 속성 검증
• 제 4 장 결론
• 참고문헌