UPPAAL을 이용한 심박수 적응 듀얼 챔버 인공심장 박동기 정형 검증

국문 초록 (Abstract)

전자기기에서의 소프트웨어 비중과 복잡도가 점점 늘어나고 있다. 이러한 현상의 일환으로 소프트웨어 자체 오류로 인한 문제 사례가 많이 보고되고 있어 소프트웨어적 결함을 개발과정에서 방지하고 품질을 향상 시켜야 한다는 전 세계적 요구가 확산되고 있다. 특히, 소프트웨어적 결함으로 생명이나 재산상의 큰 손실을 유발하는 경우 소프트웨어 품질 향상과 안전성 보장은 절대적 전제조건이 된다. 이를 위해 세계의 여러 나라는 국제 표준을 만들어 준수하고 있다. 이러한 국제 표준에서 안전성을 보장하는 방법으로 정형기법 사용을 명시하고 있다.
본 논문에서는 위의 사례로 정형기법 커뮤니티에서 선정한 문제 중 하나인 인공심장 박동기의 기본 속성을 정형기법 도구를 이용한 모델링 및 검증을 통해 안전성을 확인한다. 현재 가장 많이 사용되고 있는 심박수 적응 듀얼 챔버 인공심장 박동기(rate-adaptive dual chamber pacemaker)를 대상으로 하며, 인공심장 박동기의 기본 사항은 인공심장 박동기 과제를 관리하고 있는 McMaster 대학의 SQRL에서 제공하는 보스턴 과학의 표준 사항을 포함한 관련 의학 정보를 기준으로 한다.
인공심장 박동기는 주입 후 인공심장 박동기에 의해 발생할 수 있는 부작용이 존재한다. 현재 의학계에서는 인공심장 박동기 증후군으로 분류하고 있으며, 증후군의 종류는 운영 모드에 따라 다르게 나타난다. 이는 인공심장 박동기의 안전성에 위반되는 사항이므로, 이를 방지해야만 한다. 따라서 이를 미연에 방지하기 위해 현재 인공심장 박동기에는 제조사 마다 각각의 알고리즘을 선택적으로 사용하고 있다. 본 논문에서는 보스턴 과학의 표준 알고리즘을 바탕으로 인공심장 박동기 모델을 확장하고 인공심장 박동기 증후군의 주원인이 되는 상심실성 빈맥의 검출 모델을 포함하여 알고리즘의 정확성을 확인하고 안전성을 보장한다.

목차 (Table of Contents)

• 목 차
• 1. 서론 1
• 1.1 연구 배경 1
• 1.2 연구 목표 2
• 1.3 논문의 구성 3
• 2. 관련연구 5
• 3. 심장과 인공심장 박동기 7
• 3.1 심장 7
• 3.2 인공심장 박동기 9
• 3.2.1 인공심장 박동기 모드 10
• 3.2.2 심박수 적응 듀얼 챔버 인공심장 박동기 12
• 4. 인공심장 박동기 모델링 및 검증 15
• 4.1 UPPAAL 15
• 4.2 심박수 적응 듀얼 챔버 인공심장 박동기 모델링 18
• 4.3 심박수 적응 듀얼 챔버 인공심장 박동기 모델 검증 30
• 5. 인공심장 박동기 증후군 방지를 위한 모델 확장 39
• 5.1 상심실성 빈맥 검출 및 모드 전환 모델링 40
• 5.2 비 심방 추적 모드 모델링 46
• 5.3 확장 모델 검증 54
• 6. 결론 및 향후 과제 58
• 참고 문헌 59