초록

용어보기논문에서 용어와 풀이말을 자동 추출한 결과로, 시범 서비스 중입니다. AI-Helper

본 논문에서는 Mobile IPv6에 사이클이 있음을 Alloy로 명세(specification)하고 Alloy 분석기로 검증(verification)한 것을 해석해 보겠다. Acyclicity를 만족하지 못함으로 해서 모바일호스트는 이동을 하지 못하고 계속 사이클을 돌게 된다. Alloy는 Rational의 UML과 같은 객체모델링 언어인데, 일차논리와 집합에 기반을 둔 Z에서부터 파생되었다. Alloy는 작은 모델들을 위한 명세 언어로, Alloy 모델은 그래픽과 텍스트를 모두 지원한다. Alloy로 명세 된 것을 쉽게 분석 할 수 있는 검증도구로 Alloy 분석기가 있는데, 이러만 도구를 이용함으로써 손쉽고 빠르게 검증을 할 수 있다.

본 논문에서는 Mobile IPv6에 사이클이 있음을 Alloy로 명세(specification)하고 Alloy 분석기로 검증(verification)한 것을 해석해 보겠다. Acyclicity를 만족하지 못함으로 해서 모바일호스트는 이동을 하지 못하고 계속 사이클을 돌게 된다. Alloy는 Rational의 UML과 같은 객체모델링 언어인데, 일차논리와 집합에 기반을 둔 Z에서부터 파생되었다. Alloy는 작은 모델들을 위한 명세 언어로, Alloy 모델은 그래픽과 텍스트를 모두 지원한다. Alloy로 명세 된 것을 쉽게 분석 할 수 있는 검증도구로 Alloy 분석기가 있는데, 이러만 도구를 이용함으로써 손쉽고 빠르게 검증을 할 수 있다.

AI 본문요약

엑셀 다운로드 AI-Helper

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

• 연구 주제
• 연구 방법

문제 정의

• 그래서 Z의 일차 논리와 집합론을 기반으로 하 고, 객체지향모델의 핵심적인 사항들을 결합하여 만든 것이 Alloy이다. 본 논문에서는 1996년 IETF에 draft된 모바일 IPv6 [1]에 사이클이 있음을 Alloy로 명세하고 검 증한 것 [2]을 해석 해 보겠디..
• 모 바일 호스트가 새로운 목적지에 도착했을 때 update메시 지를 호스트에 보내고, 이 메시지가 호스트에 도착하면, 호스트의 cache를 update 시킨다. 이 논문에서는 메시 지가 호스트에 도착했을 때 캐시를 update 시키는 것으 로 사이클 있는지를 검증해보았다.

가설 설정

• 각각의 호스트는 캐시를 가지고있고, 모바일 호스트에서 최근 메시지를 보내면 그것을 캐시에 저장한다. 모바일 호스트는 단지 한 개뿐이고 분리된 모바일 호스트의 행 동들은 각각 독립적이라고 이 논문에서는 가정했다. 모 바일 호스트가 새로운 목적지에 도착했을 때 update메시 지를 호스트에 보내고, 이 메시지가 호스트에 도착하면, 호스트의 cache를 update 시킨다.

제안 방법

• 8) 이 모델은 assert B와 assert C가 똑같이 반례가 나 오지 않으므로 RefsReasonable과 LocalKnowledge의 관계를 살펴보았다.

본문요약 정보가 도움이 되었나요? 예 아니오 제출

이 논문을 인용한 문헌

더보기