권호기사보기
| 기사명 | 저자명 | 페이지 | 원문 | 기사목차 |
|---|
결과 내 검색
동의어 포함
표제지
목차
약어표 10
Abstract 11
요약 13
1. 서론 16
1.1. 연구 목적 16
1.2. 연구 목표 18
1.3. 연구 내용 19
1.4. 기여도(Contribution) 21
1.5. 논문의 구성 22
2. 관련연구 24
2.1. 정형 기법 24
2.2. 온톨로지 27
2.3. 격자(Lattice) 28
3. Prism: Behavior Ontology 31
3.1. Active Ontology 33
3.1.1. Ontology 33
3.1.2. Action 36
3.2. Behavior Ontology 38
3.2.1. Behavior 39
3.2.2. Behavior Lattice 44
3.2.3. Prism 45
4. 질의 분석 48
4.1. 클래스 종류 49
4.2. 질의 함수 50
4.2.1. 행동 관련 질의 함수 51
4.2.2. 행위 관련 질의 함수 52
4.2.3. 행위 격자 관련 질의 함수 55
4.2.4. 프리즘 관련 질의 함수 57
5. 예제 61
5.1. EMS System 소개 61
5.2. RAP(Resource Allocation Problem) Prism 62
5.2.1. RAP Active Ontology 62
5.2.2. RAP Behavior Ontology 65
5.3. EMS System 예제 1 75
5.3.1. EMS System 예제 75
5.3.2. EMS System 예제 모의 실행 결과 76
5.3.3. RAP Prism을 이용한 EMS System 예제 분석 81
5.3.4. RAP Prism을 이용한 EMS System 예제 그래픽 분석 85
5.3.5. EMS System 예제 질의 분석 88
5.4. EMS System 예제 2 94
5.4.1. 서해대교 연쇄 추돌사고 95
5.4.2. 서해대교 예제 모의 실행 결과 97
5.4.3. RAP Prism을 이용한 서해대교 예제 분석 99
5.4.4. 서해대교 예제 분석 결과 113
5.4.5. 서해대교 예제 질의 분석 115
6. 비교연구 및 활용 방안 129
1) 분석의 대상에 따른 프리즘 모델 활용 130
2) 프리즘 모델로 분석된 데이터에 대해 지식 베이스의 활용 131
3) 스케줄링 적용에 활용 132
4) 요구사항 분석 132
7. 도구 134
7.1. 프리즘 플랫폼 아키텍처 135
7.2. 프리즘 도구 화면 배치 및 기능 137
7.3. 프리즘 도구 개발 및 실행 환경 140
8. 결론 및 향후 연구 142
참고문헌 145
[그림 1.1] Prism: 프로세스 대수의 모의 실행 결과에 대한 새로운 분석 방법 18
[그림 1.2] 의미기반 행위적 분석을 위환 프리즘 19
[그림 2.1] 격자 기본 구축 예제 28
[그림 2.2] 개념 격자 예제 29
[그림 3.1] 메타 모델 단계의 프리즘 31
[그림 3.2] EMS System 온톨로지 예 34
[그림 3.3] 행동을 정의한 EMS System 온톨로지 예 37
[그림 3.4] 추상화 행위 B₁ 과 B₂의 격자 L₁ 45
[그림 3.5] P(P,A,H)에 대한 프리즘 46
[그림 4.1] 프리즘 질의 시스템 48
[그림 4.2] 모의 실행 결과로부터 프리즘 생성 예제 50
[그림 4.3] 행동 관련 질의 함수 사용 예 52
[그림 4.4] 행위 관련 질의 함수 사용 예 54
[그림 4.5] 행위 격자 관련 질의 함수 사용 예 56
[그림 4.6] 프리즘 관련 질의 함수 사용 예 58
[그림 4.7] 질의 함수를 통한 수직적 질의 사용 예 59
[그림 5.1] EMS System 분석을 위한 온톨로지 63
[그림 5.2] EMS System의 이동체에 대한 행위의 체계적 추상화 71
[그림 5.3] EMS System의 자원, 이동체, 핸들러 관점의 행위의 체계적 추상화 72
[그림 5.4] EMS System의 행위 추상화 73
[그림 5.5] EMS System 예제를 명세 도구로 명세 76
[그림 5.6] Mobile Ambients Calculus 로 명세된 EMS System 예제 (Postscript Version) 77
[그림 5.7] EMS System 그래픽 모의 실행 결과 78
[그림 5.8] EMS System 텍스트 모의 실행 결과 일부분 79
[그림 5.9] EMS System 온톨로지 81
[그림 5.10] EMS System 예제를 RAP Prism 분석 결과 84
[그림 5.11] EMS System 모의 실행 결과에 RAP 프리즘의 행동 적용 85
[그림 5.12] EMS System 모의 실행 결과에 RAP 프리즘의 행위 적용 86
[그림 5.13] EMS System 모의 실행 결과에서 모든 구급차 관점 행위 분석 87
[그림 5.14] 복합 질의 사용 예 1 89
[그림 5.15] EMS System 모의 실행 결과에서 질의를 통한 FP2의 행위 분석 91
[그림 5.16] 복합 질의 사용 예 2 92
[그림 5.17] EMS System 모의 실행 결과에서 복합 질의의 최종 분석 결과 94
[그림 5.18] 프로세스 대수 명세 도구를 사용한 서해대교 예제 명세 및 실행 97
[그림 5.19] 서해대교 예제 텍스트 모의 실행 결과 일부분 98
[그림 5.20] 서해대교 온톨로지 100
[그림 5.21] RAP 프리즘 관점 서해대교 예제 분석 101
[그림 5.22] 서해대교 예제의 구급차 A1의 행위 분석 107
[그림 5.23] 서해대교 예제의 구급차 A2의 행위 분석 109
[그림 5.24] 서해대교 예제의 구급차 A3의 행위 분석 110
[그림 5.25] 서해대교 예제의 구급차 A9의 행위 분석 112
[그림 5.26] 서해대교 예제의 RAP 프리즘 분석 결과 113
[그림 5.27] 환자 SEP32를 이송한 구급차 분석 질의 1 117
[그림 5.28] 환자 SEP32를 이송한 구급차 분석 질의 2 118
[그림 5.29] RAP 프리즘에서 환자 SEP32를 이송한 구급차 행위 분석 119
[그림 5.30] 환자 SEP32를 이송한 구급차 A6의 행위 분석 121
[그림 5.31] 식중독 환자 FP1, FP2를 이송한 구급차 분석 질의 1 122
[그림 5.32] 식중독 환자 FP1, FP2를 이송한 구급차 분석 질의 2 124
[그림 5.33] RAP 프리즘에서 식중독 환자 FP1, FP2를 이송한 구급차 행위 분석 125
[그림 5.34] 식중독 환자 FP1, FP2를 이송한 구급차들의 행위 분석 128
[그림 7.1] Onion 명세, 분석 및 검증 도구 아키텍처 134
[그림 7.2] 프리즘 플랫폼 아키텍처 135
[그림 7.3] 프리즘 도구 화면 배치 139
[그림 7.4] 프리즘 명세 139
[그림 7.5] 프리즘 질의 분석 140
시스템을 명세, 분석 및 검증하기 위한 프로세스 대수는 분석과 검증을 위해 모의 실행을 수행하고 모의 실행의 결과가 생성된다. 프로세스 대수는 시스템을 명세, 분석 및 검증으로, 시스템을 분석 및 검증하기 위해 모의 실행 결과가 생성된다. 모의 실행 결과는 명세와 실행 단계에서 프로세스들의 이동과 통신의 행위 정보를 발생되는 순서에 따라 복잡하게 나열한 것이다. 이와 같은 행위의 결과는 시스템의 규모와 복잡도 그리고 실행 단계에서 발생하는 다양한 이벤트에 의해 매우 복잡해져 이를 이해하고 분석하는데 어려움이 존재한다. 또한, 모의 실행 결과 분석은 명세 언어 도구에 종속적이어서 분석에 따른 제한이 존재한다.
본 논문은 이러한 어려움을 극복하기 위해 모의 실행 결과에 존재하는 무수한 액션들에 대해 의미를 부여하여 구조화하고, 체계적으로 추상화하여 의미를 기반으로 한 행위적 관점의 분석 방법을 제안한다. 이는 기존 개별 액션에 대해 개별적으로 분석하는 방법을 벗어나 액션들을 행위적 관점으로 분석하는 방법으로 추상화를 통한 분석의 이해도를 높여 분석하는 것이다.
행위적 관점의 의미기반 추상화 분석 방법을 위해 메타 모델인 프리즘(Prism: Behavior Ontology)을 정의하였다. 프리즘은 액티브 온톨로지(Active Ontology)를 사용한 데이터 구조화와 행위 온톨로지(Behavior Ontology)를 사용한 추상화 단계로 정의된다. 프리즘을 통하여 생성된 모델은 분석하고자 하는 대상이 지니는 의미 있는 행위의 관점으로 생성된다.
액티브 온톨로지 단계는 모의 실행 결과를 의미적으로 분석하기 위해 프로세스들이 지니는 액션들의 관계를 동사의 의미로 정의하고, 액티브 온톨로지에서는 이를 행동(Action)이라고 정의한다.
행위 온톨로지 단계는 액티브 온톨로지에서 정의된 행동을 바탕으로 모의 실행 결과를 의미 있는 다양한 행위(Behavior)로 정의하고, 복합적인 행위에 대해 분석이 가능하도록 추상화 방법인 행위 격자(Behavior Lattice)를 정의한다. 또한, 동일한 행위에 대해 다양한 행위 격자에서의 분석이 가능하도록 행위 격자들 사이의 관계를 정의한 프리즘(Prism)을 정의한다.
메타 모델을 기반으로 생성된 모델 단계의 프리즘은 모의 실행 결과를 의미적으로 구조화하고, 체계화, 추상화하여 분석하고자 하는 대상이 지니고 있는 행위에 대해 의미를 기반한 추상화의 형태로 이해 및 분석이 가능하도록 한다. 따라서 모의 실행 결과에 존재하는 분석 대상에 대해 분석 가능한 다양한 프리즘 모델을 사용하여 동일한 대상을 프리즘이 지닌 다양한 의미로 분석한다. 분석된 데이터는 질의 시스템을 통하여 다양한 형태의 질의 결과를 제공한다.
또한, 일반적인 추상화 분석 방법과 달리 프리즘이 지니는 행위 격자를 통해 행위 격자 사이의 다양한 추상화 단계의 자연스러운 상하 이동을 제공한다.
프리즘 모델로 분석된 모의 실행 결과는 유사한 대상의 분석을 위한 지식베이스로 활용이 가능하며, 하나의 액션이 아닌 의미를 기반으로 한 효율적인 스케줄링으로 제공될 수 있다. 또한 기존 개별 액션에 대해 명세 단계의 요구사항 분석 방법이 아닌 프리즘이 지닌 행위적 관점의 요구사항 분석 방법의 형태로 분석될 수 있다.
본 논문에서 제안하는 의미 기반 행위적 분석 방법은 프로세스 대수의 모의 실행 결과에 대한 분석뿐만 아니라 일반적인 데이터 분석에도 활용될 수 있을 것이다.
본 논문에서는 프리즘 이론과 모델 생성, 적용 그리고 분석을 최적화된 응급 의료 서비스 제공을 위한 EMS System 예제와 이를 확장한 서해대교 예제를 통하여 설명하고, 구현된 프리즘 도구를 통해 예제를 명세, 분석하여 프리즘의 효율성과 효용성에 대해 기술한다.| 번호 | 참고문헌 | 국회도서관 소장유무 |
|---|---|---|
| 1 | Formal methods ![]() |
미소장 |
| 2 | Communication and Concurrency, Prentice-Hall, London, 1989. | 미소장 |
| 3 | A Calculus of Mobile Processes, Part I, Report ECS-LFCS -89-85, Laboratory ofr foundations of Computer Science, Computer Science Dep., Edinburgh Univ, 1989. | 미소장 |
| 4 | A Calculus of Mobile Processes, Part Ⅱ, Report ECS- LFCS-89-86, Laboratory for foundations of Computer Science, Computer Science Dep., Edinburgh Univ, 1989. | 미소장 |
| 5 | Communicating Sequential Processes, Prentice Hall Int I, 1985. | 미소장 |
| 6 | "Formal Modeling for Security Behavior Analysis of Computer Systems," MCETECH, pp.39-59, 2008 | 미소장 |
| 7 | A Calculus for Equivalence Analysis and Verification of Distributed Mobile System Based on Abstraction, phD Dissertation, Chonbuk National Univ, 2007. | 미소장 |
| 8 | “Onion: A Graphical Language for Process Algebra,” in Computer Software and Applications Conference (COMPSAC), 2011 IEEE 35th Annual, 2011, pp. 708–711. | 미소장 |
| 9 | Formal Methods for Real- Time Computing, JohnWiley&Sons,Inc., NewYork, NY, USA, 1996. | 미소장 |
| 10 | Understanding Formal Methods. Michael G, Hinchey (Ed.), Springer- Verlag New York, Inc., Secaucus, NJ, USA, 2001. | 미소장 |
| 11 | Automatic verification of finite-state concurrent systems using temporal logic specifications ![]() |
미소장 |
| 12 | Compositional Reachability Analysis using Process Algebra. In Proceedings of Conference on Testing, Analysis and Verification, pp. 49-59, August 1992. | 미소장 |
| 13 | Deciding Bisimulation Equivalences for a Class of Non-finite-state Programs. Technical Report SICS/R-89/8908, Swedish Institute of Computer Science, August 1989. | 미소장 |
| 14 | An Automatic Verification Technique for Communicating Real-Time State Machines. Technical Report 93-04-08, Dept. of Computer Science and Engineering, Univ. of Washington, April, 1993. | 미소장 |
| 15 | State Minimization for Concurrent System Analysis Based on State Space Exploration. In Proceeding of Conference on Computer Assuance, pp. 123- 134, 1994. | 미소장 |
| 16 | State Minimization Method based on Syntatic and Semantic Pattern Abstraction, PhD Dissertation, Chonbuk national Univ, 2006. | 미소장 |
| 17 | Lattice theory, Amer. Math. Soc. Colloquium Publications, vol. 25, 1995. | 미소장 |
| 18 | “Restructuring lattice theory: an approach based on Hierarchies of concepts,” In: Ivan Reval (ed.), Ordered sets, Reidel, Dordrecht-Boston, pp.445-470, 1982. | 미소장 |
| 19 | Formal Concept Analysis: Mathematical Foundations, Springer, 1999. | 미소장 |
| 20 | A translation approach to portable ontology specifications ![]() |
미소장 |
| 21 | Emergency Medical Services: Unique Transportation Safety Challenge, TRB 87th, 2008. | 미소장 |
| 22 | A Formal Method for Specification and Analysis of Timing Properties in a Process Algebra, Master Thesis, Chonbuk National Univ, 2007. | 미소장 |
| 23 | Visual Representation of Temporal Properties in Formal Specification and Analysis using a Spatial Process Algebra ![]() |
미소장 |
| 24 | Statecharts: a visual formalism for complex systems ![]() |
미소장 |
| 25 | Petri nets: Properties, analysis and applications ![]() |
미소장 |
| 26 | “Decoupled design: building applications on the NetBeans platform,” in Companion to the 21st ACM SIGPLAN symposium on Object134 oriented programming systems, languages, and applications, Portland, Oregon, USA, 2006, pp. 631–631. | 미소장 |
| 27 | “Design and Implemantation of a Question Management System based on Concept Lattice,” JOKCA, Vol.8, No.11, pp.412-425, 2008. | 미소장 |
| 28 | “전문용어 깁나인문사회분야 온톨로지 구축에 관한 연구,” 한국정보처리학회, 제 15 회 한국정보관리학회 학술대회 논문집, pp.181-188, 2008. | 미소장 |
| 29 | A Case Study on Building Verb-Ontology : Korean Locomotion Verbs | 소장 |
*표시는 필수 입력사항입니다.
| 전화번호 |
|---|
| 기사명 | 저자명 | 페이지 | 원문 | 기사목차 |
|---|
| 번호 | 발행일자 | 권호명 | 제본정보 | 자료실 | 원문 | 신청 페이지 |
|---|
도서위치안내: / 서가번호:
우편복사 목록담기를 완료하였습니다.
*표시는 필수 입력사항입니다.
저장 되었습니다.