[논문]SPIN을 이용한 고속 네트워크 인터페이스 카드의 펌웨어 검증

진현욱; 방기석; 최진영; 유혁

SPIN을 이용한 고속 네트워크 인터페이스 카드의 펌웨어 검증
Formal Verification of MCP using SPIN 원문보기

진현욱 (고려대학교 컴퓨터학과) , 방기석 (고려대학교 컴퓨터학과) , 최진영 (고려대학교 컴퓨터학과) , 유혁 (고려대학교 컴퓨터학과)

고속 네트워크 인터페이스 카드에서 수행되는 펌웨어의 기능이 다양해지고 그 개발이 자유로워짐에 따라 체계적인 펌웨어의 정형검증이 요구된다. 본 논문은 정형검증 도구인 SPIN을 사용하여 미리넷 네트워크 인터페이스 카드에서 수행되는 펌웨어인 MCP를 정형검증하여 데이터 송신에 오류가 없음을 보인다. 이를 통해서 본 논문은 펌웨어에 대한 가능한 정형검증 방법을 보이고 SPIN의 적용 범위를 확대한다.

* AI 자동 식별 결과로 적합하지 않은 문장이 있을 수 있으니, 이용에 유의하시기 바랍니다.

문제 정의

ness)을 검증함으로써 시스템의 오류를 검사한다. 본 논문에시는 MCP의 송신 부분을 명세하고 송신 시 패킷의 손실이 일어나지 않음을 검증하였다,
본 논문은 Myrinet MC에서 수행되눈 펌웨어인 MCP를 성형 검증하였다. 검증은 MCP의 송신만을 대상으로 했으며, DFA와 PR0MELA 를 사용 해시 모델링하고 SPIN을 사용하어 검증하였다.
본 논문은 현존하는 LAN 중에서 가장 빠른 Myrinet 의 NIC 에시 수행되는 펌웨어인 MCP(Myrinet Control Program)【1]를 청형검증한다, MCP의 정형 검 중을 위한 첫 단계로 본 논문에서는 송신과성만을 보델링하고 검중한다. 성형 검 중 노子로서 는 SP0I9I을 사용한다, SPIN은 Bell 연구소에서 개발되어 널리 사용되고 있는 모델 체킹 노구로서 비동기 프루세스 시스템을 디자인하고 검증하는 데 사용된다, SPIN은 PROMELAtPRocess MEta LAnguage)〔1이라는 명세 언어를 사용하여 디자인된 명세를 받아들여 선형 시제 논리 (LTL; Linear Temporal Logic)[ll]로 정의된 정확성 (corre아.
이를 위해 그림 6의 (a) 와 같이 검증에 필요한 인수들을 정의하고 그림 6의 (b)와 같이 LTL 로 만족해야 할 조건들을 표현하였다. 이번 언구 에시上 전송의 요구가 있을 경우 전송이 이루어지는가를 확인하였다..

제안 방법

본 논문은 Myrinet MC에서 수행되눈 펌웨어인 MCP를 성형 검증하였다. 검증은 MCP의 송신만을 대상으로 했으며, DFA와 PR0MELA 를 사용 해시 모델링하고 SPIN을 사용하어 검증하였다. 검증 결과, MCP는 데이터 송신 시 패킷 손실을 야기하지 않음을 종명하였다.
본 논문은 현존하는 LAN 중에서 가장 빠른 Myrinet 의 NIC 에시 수행되는 펌웨어인 MCP(Myrinet Control Program)【1]를 청형검증한다, MCP의 정형 검 중을 위한 첫 단계로 본 논문에서는 송신과성만을 보델링하고 검중한다. 성형 검 중 노子로서 는 SP0I9I을 사용한다, SPIN은 Bell 연구소에서 개발되어 널리 사용되고 있는 모델 체킹 노구로서 비동기 프루세스 시스템을 디자인하고 검증하는 데 사용된다, SPIN은 PROMELAtPRocess MEta LAnguage)〔1이라는 명세 언어를 사용하여 디자인된 명세를 받아들여 선형 시제 논리 (LTL; Linear Temporal Logic)[ll]로 정의된 정확성 (corre아.ness)을 검증함으로써 시스템의 오류를 검사한다. 본 논문에시는 MCP의 송신 부분을 명세하고 송신 시 패킷의 손실이 일어나지 않음을 검증하였다,
앞에시 모델링된 hoslSend 와 netSend 에 대해서 데이터 송신 시 패킷 손실이 발생하는지를 검증하였다. 패킷 손실이 발생하지 않음 올 보장하려면, host Send가 UostSendGotASend 상태에서 HostSendDmaDone 상태로 전이되는 깃과 netSend 가 NetSendGotASend 상태에서 NetSendDmaDone 상태로의 전이됨이 보장되어야 한다.
이와 같이 본 논문은 고속 네트워크의 NIC에서 수행되는 펌웨어를 SPIN을 사용하여 정형 검증함으로써 펌웨어에 대한 가능한 정형 검증 방법을 보였을 뿐만 아니라, SPIN의 직용범 위를 펌웨어를 포함하는 프로토콜 계중으로 확장하였다.

대상 데이터

본 논문은 MCP의 송신 부분만을 모델링하고 검증한匸즉, 2장에서 설명되어진 hostSend 와 nelSend 만을 대상으로 한다.

성능/효과

검증은 MCP의 송신만을 대상으로 했으며, DFA와 PR0MELA 를 사용 해시 모델링하고 SPIN을 사용하어 검증하였다. 검증 결과, MCP는 데이터 송신 시 패킷 손실을 야기하지 않음을 종명하였다.

후속연구

실제로 MCP의 기능을 모두 성형검증 하기 위해서는 Receive 부분노 모델링 되고 송신과 함께 검중올 해야 한다. 이러한 작업이 모두 이루어진다면, 고속 네트워크 NIC의 오든 기능을 정형명세함으로써 MCP의 정확성 검증이 가능하리라 생각한다. 특히 메시지를 연속해서 전송하고 수신할 경우 그 순시 역시 정확성의 중요한 요소가 된다.
특히 메시지를 연속해서 전송하고 수신할 경우 그 순시 역시 정확성의 중요한 요소가 된다. 향후 수신 부분의 기능을 명세하고 MCP가 만족해야 할 특성에 대해 검증을 수행할 계획이다.

원문 보기

ScienceON 원문보기

*원문 PDF 파일 및 링크정보가 존재하지 않을 경우 KISTI DDS 시스템에서 제공하는 원문복사서비스를 사용할 수 있습니다.

내보내기 메뉴

내보내기 구분

파일저장
인쇄
메일전송

구성항목

기본정보
상세정보

관리번호, 논문명, 저널/프로시딩명, 저자 , 발행년, 권, 호, 시작페이지, 끝페이지, 발행기관

저장형식

Text(ASCII format)
Excel format
RefWorks Direct Export
RIS format (for Reference Manager, ProCite, EndNote), Scholar's Aids, Mendeley

메일정보

받는사람 (필수): @
보내는사람 (선택): @
제목
내용: KISTI 검색결과 이메일 서비스

안내

총 건의 자료가 검색되었습니다.

다운받으실 자료의 인덱스를 입력하세요. (1-10,000)

검색결과의 순서대로 최대 10,000건 까지 다운로드가 가능합니다.

데이타가 많을 경우 속도가 느려질 수 있습니다.(최대 2~3분 소요)

다운로드 파일은 UTF-8 형태로 저장됩니다.
파일의 내용이 제대로 보이지 않을실 때는 웹브라우저 상단의 보기 -> 인코딩 -> 자동선택 여부를 확인하십시오.

Text(ASCII format)
Excel format

표제어: PCR

동의어: Packet Collision Rate

용어 설명 출처 목록 (6)

용어 설명: PCR은 세균 특이성이 있는 primer를 이용하여 적은 수의 세균이 있을지라도 쉽게 검출할 수 있는 유용한 방법이며, 이를 이용하여 구강 내 치면세균막이나 타액에서 직접 세균을 검출할 수 있게 되었다[8].

AI-Helper ※ AI-Helper는 을 사용합니다.

AI-Helper

안녕하세요, AI-Helper입니다. 좌측 "선택된 텍스트"에서 텍스트를 선택하여 요약, 번역, 용어설명을 실행하세요.
※ AI-Helper는 부적절한 답변을 할 수 있습니다.

연합인증

SPIN을 이용한 고속 네트워크 인터페이스 카드의 펌웨어 검증
Formal Verification of MCP using SPIN 원문보기

초록
AI-Helper