http://chineseinput.net/에서 pinyin(병음)방식으로 중국어를 변환할 수 있습니다.
변환된 중국어를 복사하여 사용하시면 됩니다.
MANET에서 CSP/FDR을 이용한 EAODV 라우팅 프로토콜 검증
안영아(Young-Ah Ahn),전철욱(Chul-Wook Geon),김일곤(Il-Gon Kim),이명선(Myoung-Sun Lee),최진영(Jin-Young Choi) 한국정보과학회 2004 한국정보과학회 학술발표논문집 Vol.31 No.1A
MANET에서 라우팅 경로가 설정되었다고 하더라도 노드의 이동성으로 인하여 네트워크의 끊김 현상이 발생하여 재라우팅을 해야 하는 오버헤드와 전송 지연이 발생한다. 이러한 문제를 해결하기 위하여 각 노드의 에너지를 기반으로 에너지 그룹을 형성하고, 반응적 라우팅 프로토콜인 AODV를 수정하여 EAODV(Energy aware ADODV)를 제안하고 이를 정형 기법을 통해 명세하고 항상 라우팅 패스를 찾는다는 속성을 검증한다.
MANET 에서 Secure Property를 고려한 라우팅 프로토콜 연구
안영아(Young-Ah Ahn),최진영(Jin-Young Choi) 한국정보과학회 2003 한국정보과학회 학술발표논문집 Vol.30 No.2Ⅲ
MANET 환경에서 Secure Property를 만족하며 노드의 Connectivity 끊김 현상을 사전에 예견하고 또한 Power group을 형성하여 liveness을 지원한다. 또한 Authentication을 만족하기 위해 Localized Certificated 방식의 매카니즘을 이용하여 Secure 라우팅 프로토콜을 제안한다.
이수영(Su-Young lee),김진현(Jin-Hyun Kim),안영아(Youna-Ah Ahn),심재환(Jae-Hwan Sim),양진석(Jin-Seock Yang),이나영(Na-Young Lee),손한성(Han-Seong Son),최진영(Jin-Young Choi) 한국정보과학회 2004 한국정보과학회 학술발표논문집 Vol.31 No.2Ⅱ
항공 및 국방 산업 등에서는 고안전성 임베디드 시스템의 신뢰성과 안전성을 보장하기 위해 임베디드 시스템의 설계 및 구현에 정형기법을 적용하고 있다. 본 논문은 그러한 정형기법을 적용하여 임베디드 시스템 소프트웨어의 요구사항 명세(Software Requirements Specification:SRS)와 요구명세를 바탕으로 실제 구현을 위한 설계명세(Software Design Specification:SDS)를 정형기법을 이용하여 명세하였다 본 논문은 정형 명세 언어로 작성된 요구명세와 설계명세 간의 부합성 검사를 하고 더 나아가 임베디드 시스템 요구 분석에서 더 정 확하게 소프트웨어를 구현할 수 있는 방법을 제시 하고자 한다.
STATEMATE MAGNUM 모델체킹을 위한 정형명세 기법 연구
김진현(Jin Hyun Kim),안영아(Young Ah Ahn),장상철(Sang Chul Jang),이나영(Na Young Lee),최진영(Jin Young Choi) 한국정보과학회 2004 한국정보과학회 학술발표논문집 Vol.31 No.1B
STATEMATE는 Statecharts로 시스템의 행위를 설계하는 도구이다. 근래 들어. STATEMATE MAGNUM은 설계 뿐 아니라 모델체킹을 이용한 정형검증의 기능을 가지고 있다. 모델체킹은 상태 기반의 설계명세 된 시스템을 시제 논리로 그 요구 명세를 기술하여 설계명세가 요구명세를 만족시키는지를 검증하게 된다. 하지만 설계명세가 큰 경우, 모델체킹 시 상태폭발을 일으켜 시스템을 검증하지 못하게 한다. 모델체킹의 상태 폭발을 줄이기 위해서는 기본적으로 모델체커의 알고리즘을 개선시키거나, 모델을 추상화 시킨다. 본 연구에서는 모델을 추상화 시키더라도 검증 결과에는 별 영향을 주지 않는 부분을 추상화하고, 검증 결과에 직접 적인 영향을 주는 부분을 상세 명세하는 기법을 적용하여 실시간 운영체제의 코드를 어떻게 검증을 하는지를 보여준다.