Alarm과 ISR을 고려한 IoT 디바이스 제어 소프트웨어의 API 호출 제약사항 검증

김동우; 최윤자; Dongwoo Kim; Yunja Choi

연구문헌

국내 논문지

홈 > 연구문헌 > 국내 논문지 > 한국정보과학회 논문지 > 정보과학회논문지 (Journal of KIISE)

정보과학회논문지 (Journal of KIISE)

Current Result Document : 4 / 6 이전건 다음건

한글제목(Korean Title)	Alarm과 ISR을 고려한 IoT 디바이스 제어 소프트웨어의 API 호출 제약사항 검증
영문제목(English Title)	API-call Constraint Checking Considering Alarms and ISRs for IoT Device Control Software
저자(Author)	김동우 최윤자 Dongwoo Kim Yunja Choi
원문수록처(Citation)	VOL 45 NO. 12 PP. 1269 ~ 1278 (2018. 12)
한글내용 (Korean Abstract)	IoT 운영체제는 API를 사용상의 규칙과 함께 제공하며 사용상의 규칙이 위반될 경우 시스템의 무결성이 깨질 수 있고 최악의 상황인 시스템 실패까지 발생할 수 있으므로 어플리케이션은 반드시 제약사항을 준수하여 API를 사용해야 한다. 기존 연구에서는 운영체제와 어플리케이션을 정형 모델로 표현하고 모델 검증을 통하여 제약사항 위반 시나리오를 탐지하였지만 시간을 고려해야하는 Alarm이나 임의로 발생할 수 있는 인터럽트 및 ISR은 검증 대상에서 제외되어 오탐 및 미탐이 발생할 수 있는 여지가있었다. 본 연구에서는 Alarm의 실제 시간은 정형 모델의 상대시간으로 변환하고 인터럽트와 ISR은 검증모델에서 임의로 발생하도록 정의함으로써 Alarm 및 ISR을 고려한 제약사항 검증을 가능하게 하였다. 제안한 방법을 19개 IoT 어플리케이션에 적용한 결과 34개의 제약사항 위반을 탐지하였으며 15개는 Alarm 이나 ISR을 고려하지 않았을 때 탐지할 수 없는 제약사항 위반이었다.
영문내용 (English Abstract)	The IoT operating system provides a set of API functions for applications along with a set of API-call constraints and all the applications are required to use API in accordance with these constraints. Improper use of API can result in breaking of system integrity and system failure. The prior study introduced a method for API-call constraint checking by converting the operating system and application into formal models and identifying API-call constraint violation scenarios through model checking. But, Alarms that should be considered for actual time or interrupts that can occur arbitrarily were left out of the scope of the verification. This study introduces the method for verifying API-call constraints considering the Alarms and ISRs. The actual time of an alarm is converted to the relative time of the formal model, and interrupts are defined to be generated anytime to activate an ISR in the verification model. Application of the verification method to 19 IoT applications led to the detection of a total of 34 API-call constraint violations, 15 of which were not detected due to lack of consideration of Alarms and/or ISRs.
키워드(Keyword)	API API 호출 제약사항 검증 정형 검증 IoT system API API-call constraint checking formal verification IoT system
파일첨부	PDF 다운로드