[논문]CSP/FDR을 이용한 리더 선출 알고리즘의 검증

전철욱; 김일곤; 안영아; 최진영

CSP/FDR을 이용한 리더 선출 알고리즘의 검증
Verification of Leader Election Algorithm with CSP/FDR 원문보기

전철욱 (고려대학교 컴퓨터학과) , 김일곤 (고려대학교 컴퓨터학) , 안영아 (고려대학교 컴퓨터학) , 최진영 (고려대학교 컴퓨터학과)

시스템이 대형화가 되어가고 네트워크 환경이 발전함에 따라 분산 환경이 점점 더 증대되어 가고 있다. 이러한 분산 환경에서 사용되는 리더 선출 알고리즘(Leader Election Algorithm)은 다양하게 제시되었고 본 논문에서는 Garcia-Molina가 제시한 Bully 알고리즘을 프로세스 알제브라 언어인 CSP로 명세하고 FDR 모델체킹 도구를 이용해 해당 요구사항을 만족하는지 검증하였다.

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

가설 설정

2) Q가 이eaction을할 수 있게 된다.

제안 방법

분산 알고리즘을 검중하기 위해 다양한 정형 기법과 도구들이 적용되어왔다 m. 본 논문에서는 프로세스 알 제브라 언어인 CSP로 Bully 알고리즘을 명세하고 모델 체커인 FDR을 이용해서 "반드시 Coordinator가 존재한다” 요구 사항을 검중하였다. 2장에서는 Bully 알고리즘과 CSP를 소개하고 3장에서는 Bully 알고리즘을 CSP로 명세하고 FDR로 검중한 내용을 설명하고, 마지막 4장에서는 결론 및 향후 연구에 대해 논하도록 하겠다.
지금까지 CSP 라는 프로세스 알제브라 언어로 Bully 알고리즘올 명세하였고 FDR 이라는 모델체커를 이용해 “반드시 Coordinator^}- 존재해야 한다「' Property를 검증해보았다. 이러한 리더 선출 알고리즘은 wireless 환경에서 많이 사용되면 향후 연구로서는 wireless 환경에서 사용되는 리더 선출 알고리즘을 연구하고자 한다.

성능/효과

3) 만약 자신보다 높은 식별자를 가진 프로세스가 0K 웅답을 할 경우 P 프로세스의 작업은 끝이 난다.
ok는 알고리즘에서 사용되는 것과 마찬가지로 election에 응답하는 이벤트이다. 마지막으로 fail은 실제 알고리즘에는 없지만 응답 시간이 지나서 ok라는 메시지를 못 받을 경우나, 프로세스가 실행하고 았지 않은 경우 ok 라는 메시지를 보내지 못하기 때문에 fail이라는 이벤트가 생긴다고 가점해서 명세했다.

후속연구

지금까지 CSP 라는 프로세스 알제브라 언어로 Bully 알고리즘올 명세하였고 FDR 이라는 모델체커를 이용해 “반드시 Coordinator^}- 존재해야 한다「' Property를 검증해보았다. 이러한 리더 선출 알고리즘은 wireless 환경에서 많이 사용되면 향후 연구로서는 wireless 환경에서 사용되는 리더 선출 알고리즘을 연구하고자 한다.

원문 보기

ScienceON 원문보기

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

이 논문과 함께 이용한 콘텐츠

[논문] MANET에서 CSP/FDR을 이용한 EAODV 라우팅 프로토콜 검증

내보내기 메뉴

내보내기 구분

파일저장
인쇄
메일전송

구성항목

기본정보
상세정보

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

저장형식

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는 부적절한 답변을 할 수 있습니다.

연합인증

CSP/FDR을 이용한 리더 선출 알고리즘의 검증
Verification of Leader Election Algorithm with CSP/FDR 원문보기

초록
AI-Helper