| 1 |
1
복수의 노드들간의 연결 관계로 표현되는 시스템의 모델을 검증하는 방법에 있어서,
상기 모델에 대해 검증하고자 하는 제1 검증식을 만족하는 노드들을 화면에 표시하는 단계;
상기 제1 검증식을 만족하는 노드들과 주변 노드들 사이의 관계에 따라 상기 제1 검증식을 만족하는 노드들을 하나의 이상의 색으로 마킹하여 상기 화면으로 출력하는 단계; 및
상기 모델이 변화하여 상기 제1 검증식을 만족하는 노드들 중 적어도 하나의 노드와 주변 노드들 사이의 관계가 변화되면, 상기 화면에서 상기 변화된 관계에 따라 마킹된 색을 변경하는 단계
를 포함하는, 점증적 모델 검증 방법
|
| 2 |
2
제 1 항에 있어서,
상기 마킹하여 출력하는 단계는,
모델 검증 EG 알고리즘의 결과를 각각의 노드에 따라 구분하여 저장하는 단계를 포함하는, 점증적 모델 검증 방법
|
| 3 |
3
제 2 항에 있어서,
상기 마킹하여 출력하는 단계는,
상기 제1 검증식을 만족하면서 SCC를 구성하는 노드를 제1 색으로 마킹하고, 상기 제1 검증식을 만족하면서 상기 제1 색으로 마킹된 노드에 연결 가능한 노드를 제2 색으로 마킹하며, 상기 제1 검증식을 만족하면서 상기 제1 색으로 마킹된 노드에 연결될 수 없는 노드를 제3 색으로 마킹하고, 상기 제1 검증식을 만족하지 않는 노드를 제4 색으로 마킹하는 단계를 포함하는, 점증적 모델 검증 방법
|
| 4 |
4
제 2 항에 있어서,
상기 마킹된 색을 변경하는 단계는,
상기 저장된 EG 알고리즘의 결과에 상기 모델의 변화를 반영하는 단계를 포함하는 것을 특징으로 하는, 점증적 모델 검증 방법
|
| 5 |
5
삭제
|
| 6 |
6
제 2 항에 있어서,
상기 마킹하여 출력하는 단계는,
상기 제1 검증식을 만족하는 노드들을 거쳐 제2 검증식을 만족하는 노드에 도달하는 경우에 상기 제2 검증식을 만족하는 노드를 제1 색으로 마킹하고, 상기 제1 검증식을 만족하면서 상기 제1 색으로 마킹된 노드에 연결 가능한 노드를 제2 색으로 마킹하며, 상기 제1 검증식을 만족하면서 상기 제1 색으로 마킹된 노드에 연결될 수 없는 노드를 제3 색으로 마킹하고, 상기 제1 검증식을 만족하지 않는 노드를 제4 색으로 마킹하는 단계를 포함하는, 점증적 모델 검증 방법
|
| 7 |
7
삭제
|
| 8 |
8
복수의 노드들간의 연결 관계로 표현되는 시스템의 모델을 검증하는 방법에 있어서,
상기 모델에 대해 검증하고자 하는 제1 검증식을 만족하는 노드들을 화면에 표시하는 단계;
상기 제1 검증식을 만족하는 노드들과 주변 노드들 사이의 관계에 따라 상기 제1 검증식을 만족하는 노드들을 하나의 이상의 그룹으로 분류하여 상기 화면으로 출력하는 단계; 및
상기 모델이 변화하여 상기 제1 검증식을 만족하는 노드들 중 적어도 하나의 노드와 주변 노드들 사이의 관계가 변화되면, 상기 화면에서 상기 변화된 관계에 따라 상기 그룹의 분류를 변경하는 단계
를 포함하는, 점증적 모델 검증 방법
|
| 9 |
9
제 8 항에 있어서,
상기 모델은,
상기 시스템에 대해 크립케 구조를 이용하여 모델링된 것을 특징으로 하는, 점증적 모델 검증 방법
|
| 10 |
10
복수의 노드들간의 연결 관계로 표현되는 시스템의 모델을 검증하는 방법에 있어서,
소정의 모델 검증 알고리즘을 적용하여 하나의 이상의 색으로 마킹된 노드들에 관한 정보를 화면에 표시하는 단계;
상기 모델이 변화하여 제1 검증식을 만족하는 노드들 중 적어도 하나의 노드와 주변 노드들 사이의 관계가 변화되면, 상기 모델 검증 알고리즘을 적용하면서 상기 변화된 관계에 따라 마킹된 색을 상기 화면에서 변경하는 단계; 및
상기 모델 검증 알고리즘에 따른 상기 모델의 검증 성공 여부를 산출하는 단계
를 포함하는, 점증적 모델 검증 방법
|
| 11 |
11
제 10 항에 있어서,
상기 모델 검증 알고리즘은,
점증 모델 검증 기법 중 EG 알고리즘 또는 EU 알고리즘 중 어느 하나인 것을 특징으로 하는, 점증적 모델 검증 방법
|
| 12 |
12
제 10 항에 있어서,
상기 모델의 검증 성공 여부를 산출하는 단계는,
상기 제1 검증식을 만족하면서 SCC를 구성하는 노드가 제1 색으로 마킹되고 상기 제1 검증식을 만족하면서 상기 제1 색으로 마킹된 노드에 연결 가능한 노드가 제2 색으로 마킹된 상태에서, 상기 모델의 시작 노드가 상기 제1 색 또는 제2 색의 노드에 직접 연결된 경우, 검증에 성공한 것으로 판단하는 단계를 포함하는, 점증적 모델 검증 방법
|
| 13 |
13
제 10 항에 있어서,
상기 모델의 검증 성공 여부를 산출하는 단계는,
상기 제1 검증식을 만족하는 노드들을 거쳐 제2 검증식을 만족하는 노드에 도달하는 경우에 상기 제2 검증식을 만족하는 노드가 제1 색으로 마킹되고 상기 제1 검증식을 만족하면서 상기 제1 색으로 마킹된 노드에 연결 가능한 노드가 제2 색으로 마킹된 상태에서, 상기 모델의 시작 노드가 상기 제1 색 또는 제2 색의 노드에 직접 연결된 경우, 검증에 성공한 것으로 판단하는 단계를 포함하는, 점증적 모델 검증 방법
|
| 14 |
14
제 1 항 내지 제 13 항 중 어느 한 항에 따른 점증적 모델 검증 방법을 컴퓨터 시스템에서 실행하기 위한 프로그램이 기록된 컴퓨터 시스템이 판독할 수 있는 기록매체
|
