| 1 |
1
융합 서비스와 시멘틱 규칙을 모델링하는 융합 서비스 모델링부;상기 모델링된 융합 서비스와 시멘틱 규칙을 모델 체커의 시스템 모델인 입력 코드와 선형 시제 논리식으로 변환하는 융합 서비스 변환부; 및상기 변환된 입력 코드 및 선형 시제 논리식을 대상으로 모델 체킹을 통해 서비스 충돌을 탐지하고 서비스 충돌원인을 분석하는 서비스 충돌탐지 및 원인 분석부;를 포함하고,상기 융합 서비스 모델링부는,서비스 유효조건을 그 특성에 따라 전제조건(Precondition), 정책(Policy) 및 가정(Assumption)으로 구분하여 기술하며,전제조건(Precondition), 정책(Policy) 및 가정(Assumption)은 각각 서비스의 시작 이전, 실행 도중, 그리고 항상 만족해야 하는 제약조건을 나타내는 것을 특징으로 하는 융합 서비스 충돌탐지 장치
|
| 2 |
2
제 1 항에 있어서, 상기 융합 서비스 모델링부는도메인 온톨로지에 기반하여 융합 서비스를 모델링하고, 융합 서비스의 유효조건을 시맨틱 규칙으로 기술하는 것을 특징으로 하는 융합 서비스 충돌탐지 장치
|
| 3 |
3
삭제
|
| 4 |
4
제 1 항에 있어서, 상기 융합 서비스 변환부는융합 서비스의 충돌원인 식별을 위해 융합 서비스와 시맨틱 규칙 명세 및 도메인 온톨로지로부터 공유자원 및 이와 관련된 서비스 정보를 추출하는 것을 특징으로 하는 융합 서비스 충돌탐지 장치
|
| 5 |
5
제 1 항에 있어서, 상기 융합 서비스 변환부는융합 서비스를 Promela로 변환하되, 융합/단위 서비스 및 Effect의 변환과 컨트롤 플로우의 변환 및 데이터 플로우의 변환을 수행하는 것을 특징으로 하는 융합 서비스 충돌탐지 장치
|
| 6 |
6
제 1 항에 있어서, 상기 융합 서비스 변환부는시맨틱 규칙을 Promela 혹은 LTL 코드로 변환하는 것을 특징으로 하는 융합 서비스 충돌탐지 장치
|
| 7 |
7
제 1 항에 있어서, 상기 서비스 충돌탐지 및 원인 분석부는융합 서비스의 충돌탐지 및 원인식별을 위해 Promela 및 LTL 코드를 모델 체커인 SPIN에 적용하여 모델 체킹을 수행하며,상기 SPIN은 서비스 충돌탐지 시 반례(counter example) 및 이에 대한 트레이스(trace) 정보를 생성하며,상기 융합 서비스 충돌탐지 및 원인 분석부는 SPIN의 트레이스 정보를 사용하여 충돌 원인을 식별하는 것을 특징으로 하는 융합 서비스 충돌탐지 장치
|
| 8 |
8
제 7 항에 있어서, 상기 서비스 충돌탐지 및 원인 분석부는SPIN의 트레이스 정보로부터 충돌과 관련된 공유자원을 식별하고 공유자원 및 서비스 정보를 이용하여 충돌 원인을 식별하는 것을 특징으로 하는 융합 서비스 충돌탐지 장치
|
| 9 |
9
융합 서비스 모델링부에서, 융합 서비스와 시멘틱 규칙을 모델링하는 단계;융합 서비스 변환부에서, 모델링된 융합 서비스와 시멘틱 규칙을 모델 체커의 시스템 모델인 입력 코드와 선형 시제 논리식으로 변환하는 단계; 및서비스 충돌탐지 및 원인 분석부에서, 변환된 입력 코드 및 선형 시제 논리식을 대상으로 모델 체킹을 통해 서비스 충돌을 탐지하고 서비스 충돌원인을 분석하는 단계;를 포함하고,상기 모델링하는 단계는,서비스 유효조건을 그 특성에 따라 전제조건(Precondition), 정책(Policy) 및 가정(Assumption)으로 구분하여 기술하며, 전제조건(Precondition), 정책(Policy) 및 가정(Assumption)은 각각 서비스의 시작 이전, 실행 도중, 그리고 항상 만족해야 하는 제약조건을 나타내는 것을 특징으로 하는 융합 서비스 충돌탐지 방법
|
