표제지
초록
목차
약어목록 13
1. 서론 14
1.1. 연구 개요 14
1.2. 연구 동기 및 범위 16
1.3. 논문의 구성 18
2. 관련 연구 19
2.1. AFDX 19
2.2. 출판/구독 모델 21
3. 소스코드 정적 분석을 통한 출판/구독모델 기반 시스템과 AFDX 결합 방법론 23
3.1. 소스코드 정적 분석을 통한 네트워크 속성 값 추출 24
3.2. Frama-C 한계의 원인 분석 및 해결안 제시 26
3.3. 소스코드 재구성 및 정적 분석 27
4. 결과 분석 29
4.1. 예제 코드 분석 29
4.1.1. PX4 무인기 예제 프로그램 29
4.1.2. ROS Robot Localization 예제 프로그램 30
4.1.3. ROS Automatic Pilot 예제 프로그램 31
5. 결론 및 향후 연구 계획 32
참고문헌 33
SUMMARY 35
Table 2A. 가상링크 파라미터 21
Table 2B. 가상 링크의 대역폭 수식 표현 21
Fig. 2.1. AFDX Topology 19
Fig. 2.2. 출판/구독 모델 22
Fig. 3.1. 출판 함수 분석을 통한 AFDX 설정 자동 생성 25
Fig. 3.2. 요약 현상으로 인한 분석 결과의 모호성 26
Fig. 3.3. CIL Layer를 추가한 모델 27
Fig. 4.1. PX4 Frama-C 결과 29
Fig. 4.2. PX4: Virtual Link Config File 30
Fig. 4.3. Robot Localization Frama-C 결과 30
Fig. 4.4. Robot Localization: Virtual Link Config File 31
Fig. 4.5. Robot Autopilot Frama-C 결과 31
Fig. 4.6. Robot Autopilot: Virtual Link Config File 31