선택한 단어 수는 입니다.
최소 단어 이상 선택하여야 합니다.
최소 단어 이상 선택하여야 합니다.
선택한 단어 수는 30입니다.
최대 10 단어까지만 선택 가능합니다.
최대 10 단어까지만 선택 가능합니다.
제안 방법
- 본 연구에서는 차량 전장용 운영체제의 표준을 따라 정의한 모델과 그 표준에 맞는 환경 설정을 활용하여, 모델 검증할 대상이 되는 차량 전장용 제어 프로그램에서 정의한 Task 시나리오를 모의실험 한 후, 각 Task의 상태의 변화를 확인하여 그에 대한 오류를 사전에 확인 할 수 있는 모의실험 및 결과 가시화 도구를 Spin 모델 검증기를 기반으로 개발하였다. 이전에 개발된 NuSMV 모델 검증기를 기반으로 개발한 도구와 비교하여 실험을 하였을 때 두 도구 간 성능으로써의 차이점을 볼 수 있었으며, 또한 비교 과정에서 동일한 제어 소프트웨어를 공통적인 절차의 흐름에 따라 또 다른 특정 모델 기반의 모의실험 및 가시화 도구를 개발할 수 있는 가능성을 확인하였다.
- 모델 검증이란 대상 시스템 내에서 일어날 수 있는 모든 행위를 탐색하는 검증 기술을 말한다. 모든 가능한 시스템 시나리오들을 모델 검증 도구를 통해 모의실험을 하며, 특정 속성에 대한 만족 여부를 알 수 있다.
- 본 도구는 OSEK/VDX 표준에 대한 환경 설정을 위해 OSEK/VDX 구현 언어(OIL)로 작성된 코드를 사용하여 ProMeLa로 미리 작성된 차량 전장용 운영체제 모델 코드에 적용을 한다. 이 OIL로 작성된 코드는 Task, Resource, 그리고 Event에 대한 속성들과 OSEK/VDX 운영체제의 실행 환경에 대한 속성들이 기술되어 있으며, 이는 ProMeLa로 최종적으로 작성되는 모델을 가상 수행 시 Task 스케줄링에 대한 요소 사용된다.
- 이를 수행하기 위해서 Melon은 어플리케이션을 CFG의 형태로 생성하고, 깊이 우선탐색을 하여 모든 실행경로를 파악하며, 각 실행경로에서 API 호출을 추출하여 API 호출 시퀀스를 만든 후 각 API 호출 시퀀스를 검증한다.
- 본 도구에서는 Melon의 API 호출 시퀀스 추출 모듈을 활용하여 각 Task의 API 호출 시퀀스를 파악하였으며, 이와 운영체제 모델을 함께 연동하여 모의실험 모델을 생성한다.
- 우선 OSEK/VDX 표준에 맞춘 ProMeLa로 작성된 운영체제 모델을 생성하기 위해 선행 연구에서 개발된 도구[3]를 통해 검증 대상 프로그램 코드에서 각 task 별 API 호출 순서를 추출한 후 이를 가공하여 운영체제 모델 코드를 완성한다. 이 때 Task, Resource, Event 등의 환경 정보 역시 적용된다.
- Spin 검증 결과출력물을 한 줄씩 분석하는데 이 때 각 줄을 특정한 정규표현식으로 검사한다. 예를 들어 “Send 1,ActivateTask,2,0 -> queue 1 (api_ch)”라는 문장의 경우 TrailElement의 callerNumber는 1이되며, OsekApiKind는 ActivateTask이, 그리고 parameter1의 값은 2로 하여 TrailElement 객체를 완성한 후, 이 객체들을 List로 TrailWrapper가 가지고 있는다.
- 이 TrailElement 객체들 각각은 Task 모의실험 상에서 각각의 Simulation 수행 중의 시점 별 정보를 제공하며, 정보 중 Task들의 상태 및 호출된 API 정보를 시각화하는데 이용한다. TrailElement 리스트에서 인접한 객체 간 Task 상태 변화 및 그 원인이 되는 API 호출자와 그 매개변수를 막대그래프 형식으로 나타내도록 하였다.
- 모델 검증 성능을 비교하기 위해 NuSMV Task Simulation과 Spin Task Simulation 도구로 모델 검증하는데 소요되는 시간을 측정하였다. 표 1은 두 도구로 각 대상 프로그램들을 시뮬레이션하였을 때 걸린 시간을 비교한 것이다.
대상 데이터
- 실험에서는 임의로 생성된 검증대상들을 본 도구에 입력하여 모의실험을 통한 결과를 NuSMV Task Simulation 도구와 비교 및 분석하였다. 실험 대상들은 C 언어로 작성된 프로그램 코드이며 약 100 LOC 정도이다.
데이터처리
- 이 때, 운영체제 모델은 미리 정의되어 있어 모델에 대한 작업은 따로 필요가 없으며, 환경 설정에 따라 이 모델에 차량 전장용 응용 프로그램 소스코드로부터 추출된 Task의 속성들을 적용하여 최종적으로 Task를 모의 실험할 ProMeLa 기반 운영체제 모델을 생성한다. 이를 Spin을 통해 Task를 모의로 실험한 결과에 대한 상태 변이에 대한 정보를 분석하여 그 결과를 GUI를 통해 시각적으로 보여준다. 각 부분에 대한 상세설명은 다음 장에서 한다.
-
2. 실험
실험에서는 임의로 생성된 검증대상들을 본 도구에 입력하여 모의실험을 통한 결과를 NuSMV Task Simulation 도구와 비교 및 분석하였다
. 실험 대상들은 C 언어로 작성된 프로그램 코드이며 약 100 LOC 정도이다.
이론/모형
- 최종 ProMeLa 모델을 생성하기 위해, 선행 연구에서 개발한 도구인 Melon[3]을 이용하여 검증 대상 프로그램의 소스코드로부터 Task 별 API 호출 순서를 추출하였다.
- 최종적으로 생성된 ProMeLa 기반 운영체제 모델은 그림 5와 같은 구조로 되어 있으며, 이 모델을 대상으로 Spin 모델 검증 도구를 이용하여 본 모의 실험을 수행한다.
- 본 도구는 Java 언어를 기반으로 하였으며 통합 개발 IDE인 Eclipse를 사용하였다.
- 이렇게 완성된 ProMeLa 모델을 Spin Model Checker를 이용해 검증을 시도한다. 이 때, 각 Task간에는 메시지 채널링이 일어나면서 API 호출을 모방한다.
※ AI-Helper는 부적절한 답변을 할 수 있습니다.