메뉴 건너뛰기
.. 내서재 .. 알림
소속 기관/학교 인증
인증하면 논문, 학술자료 등을  무료로 열람할 수 있어요.
한국대학교, 누리자동차, 시립도서관 등 나의 기관을 확인해보세요
(국내 대학 90% 이상 구독 중)
로그인 회원가입 고객센터 ENG
주제분류

추천
검색
질문

논문 기본 정보

자료유형
학술저널
저자정보
저널정보
Korean Institute of Information Scientists and Engineers (구)정보과학회논문지 정보과학회논문지 제17권 제2호
발행연도
1990.4
수록면
212 - 225 (14page)

이용수

표지
📌
연구주제
📖
연구배경
🔬
연구방법
🏆
연구결과
AI에게 요청하기
추천
검색
질문

초록· 키워드

오류제보하기
시간에 의존하게 되는 Computer network protocol을 나타내기 위해서 state transition system을 나타내기 위한 표기법을 사용한다. Protocol의 특성을 나타내고 증명하기 위한 이 표기법은 linear-time temporal logic을 기초로 한다. 이러한 특성에 대한 증명은 작은 갯수의 추론법칙들을 이용할 수 있다.
Protocol 검증에 대한 다른 방법은 reachability graph를 이용하는 것이다. 이 방법을 이용한 검증은 reachability graph를 조사해 봄으로써 쉽게 행해질 수 있다.
이 논문에서는 위의 두가지 방법이 temporal logic을 이용한 방법을 중심으로 비교 분석되며, 왜 temporal logic을 이용한 검증 방법 또한 비 실용적인지 보여준다.

목차

요약

ABSTRACT

1. Introduction

2. Related Work

3. Notation

4. Properties

5. Proof Rules used in Verification

6. Protocol Verification using Reachability Graph

7. Verification about Master-Slave Protocol with Reliable FIFO Channel

8. Verification for the Alternating-Bit Protocol

9. Discussions for Two Protocol Verification Methods

10. Bibliography

11. Appendix

저자소개

참고문헌 (0)

참고문헌 신청

함께 읽어보면 좋을 논문

논문 유사도에 따라 DBpia 가 추천하는 논문입니다. 함께 보면 좋을 연관 논문을 확인해보세요!

이 논문의 저자 정보

최근 본 자료

전체보기

댓글(0)

0

UCI(KEPA) : I410-ECN-0101-2009-569-017777072