http://chineseinput.net/에서 pinyin(병음)방식으로 중국어를 변환할 수 있습니다.
변환된 중국어를 복사하여 사용하시면 됩니다.
GCSR의 UML - RT 언어로의 제안을 위한 STATECHART와의 비교
김진현(Jin-Hyun-Kim),박명환(Myung-Hwan-Park),최진영(Jin-Young-Choi),강인혜(Inhye-Kang) 한국정보과학회 1999 한국정보과학회 학술발표논문집 Vol.26 No.2Ⅰ
본 논문은 UML-RT 도구로서 GCSR(Graphical Communicating Shared Resource)를 제안하는데 있어 기존의 UML의 기본 다이아 그램 중 하나인 Statechart 와 비교 분석함으로 그 기능과 장단점을 제시한다. 기존의 정형 명세 언어인 Statechart 에서는 실시간 시스템의 명세에 있어 필수적인 시간적인 개념과 우선순위 개념이 제한적이다. 그러나 정형명세의 또 다른 언어인 GCSR 이 가진 시간적 개념과 우선순위 개념의 효용을 보이고 이를 Statechart 의 실시간 시스템의 명세와 비교함으로 UML-RT로서의 GCSR을 제안한다.
문영주(Young-Joo Moon),방기석(Ki-Seok Bang),김일곤(Il-Gon Kim),강인혜(Inhye Kang),최진영(Jin-Young Choi) 한국정보과학회 2005 한국정보과학회 학술발표논문집 Vol.32 No.1
전자지불 시스템의 활용성 증대와 더불어 상거래의 안전성을 보장하는 문제가 중요한 핵심 사항으로 간주되고 있다. 본 논문에서는 이러한 전자지불 시스템의 암호화 키는 안전하다는 가정 하에 전자지불 프로토콜을 통해 소비자와 상인, 은행간의 상거래의 정확성을 중점으로 NetBill 프로토콜을 명세, 검증했다. 프로토콜의 명세를 위해서는 실시간 개념이 포함되어 있는 UPPAAL을 사용했다.
Esterel 기반 임베디드 소프트웨어의 신뢰성 향상을 위한 개발 기법
양진석(Jin-Seok YANG),심재환(Jae-Hwan SIM),김진현(Jin-Hyun KIM),강인혜(In-Hye KANG),최진영(Jin-Young CHOI) 한국정보과학회 2005 한국정보과학회 학술발표논문집 Vol.32 No.1
본 논문은 정형 명세 언어인 Esterel이 가지는 취약점을 보안하기 위해 Safety-Critical Aided Development Environment를 추가로 활용하여 신뢰성 있고 안전적인 임베디드 제어 소프트웨어 개발을 위한 기법을 제시하고 있다. 그 뿐만 아니라 제시한 기법을 이용하여 개발된 간단한 자동 감속 제어 소프트웨어를 인터페이스와 기능 부분에 대해서 각각 확인 및 검증을 수행한 후 임베디드 시스템인 레고 마인드 스톰으로 제작된 차량 로봇에 탑재한 후 실험을 하고, 실험을 통해 기존 개발 기법과의 차이점을 분석한다.
강미영 ( Mi-young Kang ),김일곤 ( Il-gon Kim ),최진영 ( Jin-young Choi ),강인혜 ( In-hye Kang ),강필용 ( Pil-yong Kang ),이완석 ( Wan S. Yi ),( Dmitry P. Zegzhda ) 한국정보처리학회 2004 한국정보처리학회 학술대회논문집 Vol.11 No.1
보안 시스템에서 접근 통제 모델을 사용하는 가장 중요한 목적은 시스템 및 사용자에 대한 안정성을 보장하기 위해서이다. 본 논문에서 다루고 있는, SPR은 보안 시스템의 행위를 유한 상태 기계(FSM)기반의 보안모델로 표현한 후, 보안 모델에 대한 초기 상태의 안전성을 검사하고 초기 상태에서 다음 상태로 전이가 존재할 경우에 그 상태들에 대응하는 모든 상태들에 대해서 보안기준을 만족하는지 검증하는 도구이다. 본 논문에서는 SPR를 사용하여 현재 많은 사람들이 이용하는 Windows 운영 체제의 NTFS에 기반을 둔 보안모델의 안전성을 검증하는 방법을 소개한다.
SPSL을 이용한 NTFS 다중 사용 권한에 대한 명세 및 검증
강미영(Mi-young Kang),김일곤(Il-Gon Kim),최진영(Jin-Young Choi),강인혜(In-Hye Kang),강필용(Pil-Yong Kang),이완석(Wan S. Lee),Dmitry Zegzhda(Dmitry P. Zegzhda) 한국정보과학회 2003 한국정보과학회 학술발표논문집 Vol.30 No.2Ⅰ
시스템의 안전성을 평가하기위해 프롤로그 기반의 명세 언어인 SPSL을 사용하여 보안 모델을 정형적으로 설계하였다. 보안 모델을 시스템의 3가지 컴포넌트, 시스템 보안 상태(system security states), 접근 통제 규칙(access control rules), 그리고 보안 기준(security criteria)으로 구성된다. 본 논문에서는 NTFS의 다중 사용 권한에 대한 보안 모델을 만들어서 3가지 컴포넌트를 면세하고 안전성 문제 해결 도구인 SPR[1]을 이용하여 검증하였다.
황대연(Dae-Yon Hwang),강인혜(Jin-Young Choi),강필용(In-Hye Kang),이완석(Pil-Yong Kang),최진영(Wan S. Lee) 한국정보과학회 2003 한국정보과학회 학술발표논문집 Vol.30 No.2Ⅰ
컴퓨터 시스템에 대한 보안의 필요성이 계속적으로 증대되고 있으며 이에 다양한 보안시스템들이 개발되고 있다. 이러한 보안 시스템들이 높은 등급의 평가를 받기위해서는 정형적 방법론을 사용하여 명세 및 검증을 해야 한다. 본 논문에서는 정형 검증의 한 방법론인 모델 체킹을 이용하여 접근통제모델을 설계하고 검증하는 방법을 제안하고자 한다.
네트워크 기반 시스템 명세 및 검증을 위한 Z 프레임워크
신지훈(JeeHoon Shin),최진영(Jin-Young Choi),강인혜(Inhye Kang),고병령(Byung Ryung Koh) 한국정보과학회 2012 정보과학회 컴퓨팅의 실제 논문지 Vol.18 No.2
정형명세 언어인 Z는 상태기반의 명세언어로써 시스템의 기능성을 명세 및 검증하는데 사용되고 있다. Z를 사용하여 시스템 명세 시 Z에서 제공하는 스키마를 이용하여 복잡한 구조의 상태를 나타내기에 용이하다. 하지만 Z에서 커버하는 명세 대상이 단일 시스템이기 때문에 2개 이상의 시스템으로 구성된 네트워크 상의 통신을 나타내기가 힘든 단점이 있다. 본 논문에서는 Z를 이용하여 네트워크 환경의 시스템들의 기능 및 통신을 명세하기 위한 프레임워크를 제시하고 사례연구를 통해 Z를 통해 시스템의 기능성 및 통신을 모두 명세하여 프레임워크의 적용가능성을 살펴본다. 또한 두 가지 측면을 모두 포함하는 검증 속성을 나타냄으로써 네트워크 환경 시스템의 속성을 프레임워크를 통해 명세, 검증 가능함을 보인다. Formal specification language Z is a statebased language and used for specifying and verifying system functionalities. By using Z for specifying system, developer can easily describe a complex state through a schema in Z but, the communication in network including more than two systems is not possible to be specified. In this paper, we propose the Z framework for representing communication and functionality of systems in a networked environment and show applicability of the framework by specifying both communication and functionality of safety-critical real system, hydrogen monitoring system. The many properties which system must hold have functionality and communication simultaneously so in case study, we describe verification property including two aspects and show possibility of specifying and verifying properties in networked environment using framework.
박명환(Myung-Whan Park),김영미(Young-Mi Kim),김진현(Jean-Hyun Kim),강인혜(Inhye Kang),최진영(Jin-Young Choi) 한국정보과학회 1999 한국정보과학회 학술발표논문집 Vol.26 No.2Ⅰ
본 논문에서는 정형명세 언어인 Statechart의 의미론을 프로세스 알제브라로 설명하는 방법을 제시한다. 이렇게 함으로써 두개의 Statechart 명세간의 bisimulation 을 정의할 수 있게 된다.
김일곤(Il-Gon Kim),문영주(Young-Joo Moon),김현석(Hyun-Seok Kim),강인혜(In Hye Kang),최진영(Jin-Young Choi) 한국정보과학회 2005 한국정보과학회 학술발표논문집 Vol.32 No.1
스마트 카드 보급의 확산과 더불어 CEPS(Common Electronic Purse Specification) 전자지갑 규제표준을 기반으로 한 전자상거래 서비스의 개발이 활성화 되고 있다. 전자상거래 프로토콜은 그 특성상, 소비자와 상인간의 정확한 물품 거래가 이루어져야 할 뿐만 아니라, 문제 발생시 상호간의 원인규명을 판단하기 위한 기준이 마련되어 있어야 한다. 본 논문에서는 CSP 언어를 이용하여 CEPS 기반 전자상거래 프로토콜의 행위를 정형 명세하였고, FDR 도구를 이용하여 전자상거래 관점에서 문제점을 분석해 보았다.
김일곤(Il-Gon Kim),최진영(Jin-Young Choi),강인혜(In-Hye Kang),강필용(Pil-Yong Kang),이완석(Wan S. Lee),Dmitry P. Zegzhda(Dmitry P. Zegzhda) 한국정보과학회 2003 한국정보과학회 학술발표논문집 Vol.30 No.2Ⅰ
보안 시스템에 대해서 고등급 평가를 받기 위해서는 정형적 방법론을 사용하여, 보안 모델을 설계하고, 보안 속성을 정확히 기술해야만 한다. 본 논문에서는 정형적 설계 방법을 통해 보안모델을 설계하고 검증하기 위한, SPR(Safety Problem Resolver) 정형검증도구의 검증방법 및 기능에 대해 소개하고자 한다.