UPPAAL을 사용한 CAN 데이터베이스 검증 프레임워크
- 주제(키워드) Controller Area Network , CAN , DBC , formal verification , UPPAAL , model checking
- 발행기관 고려대학교 대학원
- 지도교수 최진영
- 발행년도 2018
- 학위수여년월 2018. 2
- 학위구분 석사
- 학과 대학원 자동차융합학과
- 세부전공 전자제어학 전공
- 원문페이지 35 p
- 실제URI http://www.dcollection.net/handler/korea/000000079708
- 본문언어 한국어
- 제출원본 000045932402
초록/요약
세계적으로 가장 많이 사용되는 차량 내 네트워크인 CAN 네트워크에서는 여러 개의 제어기가 하나의 버스를 공유하기 때문에, 메시지 응답 시간의 지연이 불가피하다. 자동차는 대표적인 안전 필수 시스템 중 하나로, CAN 네트워크에서의 메시지 응답 시간이 지연되어 마감 시간을 초과하는 경우 운전자와 차량 전체의 안전성이 훼손될 수 있다. 그러므로 운전자 및 차량의 안전과 관련된 메시지는 응답 시간의 지연이 최소화되어야 하며, 메시지의 응답 시간이 마감 시간을 초과하지 않는지 CAN 데이터베이스를 사전에 검증하는 작업이 반드시 필요하다. 본 논문에서는 차량 내 네트워크의 종단 간 메시지 응답 시간 보장에 대한 첫 번째 연구로써, CAN 네트워크에서의 메시지 응답 시간의 보장을 검증한다. 이를 위하여, 정형 명세 및 검증 도구인 UPPAAL과 CAN 데이터베이스로부터 UPPAAL 모델을 자동 생성하는 DBC2XML 컴포넌트로 구성된 프레임워크를 제안한다.
more목차
제 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 장 결론
참고문헌
