| 1 |
1
오토마타 모델내에 어떠한 천이도 존재하지 않는 deadlock 상태와 상태의 부분집합만을 무한히 반복하여 초기상태로 돌아가지 못하는 livelock 상태 혹은 상태집합이 존재하는지를 검사하는 안전성 검정 과정과, 상기 오토마타 모델의 임의의 상태에서 같은 행위에 의한 둘 이상의 천이가 존재하는 비결정성을 검정하는 결정성 검정 과정과, 상기 오토마타 모델 내의 임의의 상태에서 입력 행위와 출력 행위의 발생여부를 검사하는 상태도달성 검정을 위하여 Modal mu-calculus의 논리식으로 표현된 상태도달성 특성을 오토마타가 만족하는지를 모형 검사의 기법을 통하여 확인하는 상태도달성 검정 과정과, 상기 오토마타 모델에서 연속적인 세가지 행위가 명세내에서 과연 발생하는지를 검사하는 행위도달성 검정을 위하여 Modal mu-calculus의 논리식으로 표현된 행위도달성 특성을 오토마타가 만족하는지를 모형 검사의 기법을 통하여 확인하는 상태도달성 검정 과정을 포함하여 이루어지는 것을 특징으로 하는 유한 오토마타 기반의 프로토콜 명세에 대한 검정 방법
|
| 2 |
2
제 1 항에 있어서, 상기 안전성 검정 과정은 오토마타의 각각의 상태에 대한 레이블을 초기화시키는 단계와, 초기화된 오토마타 레이블에서 오토마타의 각 상태에 대한 천이에 따라 레이블을 갱신하는 그래프 재표기 단계와, 레이블이 갱신된 오토마타의 상태중에서 안전성을 만족하지 않는 상태들을 검출하는 안전성 검사단계를 포함하여 이루어지는 것을 특징으로 하는 유한 오토마타 기반의 프로토콜 명세에 대한 검정 방법
|
| 3 |
3
제 1 항에 있어서, 상기 결정성 검정 과정은 결정성 여부를 확인하는 변수를 결정형으로 설정하고, 비결정형 행위와 상태 번호를 가지는 변수를 선언하는 단계와, 오토마타의 상태 개수와 상태의 천이갯수만큼 결정성 검사를 수행하는 단계와, 다른 시점에 같은 천이가 존재하는지를 검사하는 단계와, 다른 시점에 같은 천이가 존재하면 상기 결정성 여부를 확인하는 변수값을 비결정형으로 설정하고, 해당 천이와 상태를 각각 변수에 삽입하고, 처리하지 않은 상태와 천이가 없을 때까지 반복하는 단계와, 처리하지 않은 상태가 없을 경우 상기 결정성 여부를 확인하는 변수값을 리턴하고 종료하는 단계를 포함하여 이루어지는 것을 특징으로 하는 유한 오토마타 기반의 프로토콜 명세에 대한 검정 방법
|
| 4 |
4
제 1 항에 있어서, 상기 상태도달성 검정 과정은 오토마타를 입력받고 사용자로부터 키보드로 검정상태, 들어오는 행위1 및 나가는 행위2를 입력받아, 상태도달성 블럭을 초기화하는 단계와, 에지 레이블화 그래프, M 배열 및 비트 배열을 생성하는 단계와, 상기 비트 배열을 초기화 및 갱신하고, M 배열에 <상태,변수>짝을 선입선출 큐로 저장하는 단계와, 필연성 알고리즘을 수행하는 단계를 포함하여 이루어지는 것을 특징으로 하는 유한 오토마타 기반의 프로토콜 명세에 대한 검정 방법
|
| 5 |
5
제 4 항에 있어서, 상기 블럭 초기화 과정은 오토마타와 사용자로부터 키보드로 검사상태, 들어오는 행위1 및 나가는 행위2를 차례로 입력받아 상태도달성에 해당하는 논리식에 따른 최대 고정 소수점 블럭과 최소 고정 소수점 블럭으로 나누어 해당 변수를 생성하는 것을 특징으로 하는 유한 오토마타 기반의 프로토콜 명세에 대한 검정 방법
|
| 6 |
6
제 4 항에 있어서, 상기 에지 래이블화 그래프 생성 과정은 B
|
| 7 |
7
제 4 항에 있어서, 상기 비트 배열 초기화 방법은 맥스 블럭 좌변의 변수 Xi와 관련된 비트-벡터값을 true로 초기화한 후, 오퍼레이터의 타입을 검사하여, 우변이 atomic proposition이고, 상태 Xi가 그 atomic proposition을 만족하지 않으면 false로 초기화하고 M[max]에 <S,Xi>를 추가하며, 우변이 <a>Xj형태이고, 상태 Si가 a천이를 가지지 않으면 false로 초기화하고 M[max]에 <S, Xi>를 추가하므로써 맥스 블럭을 초기화하는 단계와, 민 블럭 좌변의 변수 Xi와 관련된 비트-벡터값을 false(0)로 초기화하고, 오퍼레이터의 타입을 검사하여, 우변이 atomic proposition이고, 상태 Si가 atomic proposition을 만족하면 true로 초기화하고 M[min]에 <S, Xi>를 추가하므로써 민 블럭을 초기화하는 단계를 포함하여 이루어지는 것을 특징으로 하는 유한 오토마타 기반의 프로토콜 명세에 대한 검정 방법
|
| 8 |
8
제 4 항에 있어서, 상기 필연성 검정 과정은 M[max]가 빌 때까지, <상태, 변수>짝을 하나씩 추출하고, Xi→Xj의 변수 상관관계에서 오퍼레이터가 만약 Xi∨Xj 또는 Xi∨Xj인 Xj가 max block의 좌변에 존재하고, S
|
| 9 |
9
제 1 항에 있어서, 상기 행위도달성 검정 과정은 오토마타를 입력받고, 사용자로부터 키보드로 행위1, 행위2, 행위3을 입력받아, 행위도달성 블럭을 생성하고 초기화하며, 이에 따라 에지 래이블화 그래프, M 배열 및 비트 배열을 생성하는 단계와, 상기 비트 배열을 초기화시키고 상기 M 배열에 <상태,변수>짝을 선입선출 큐로 저장하는 단계와, 필연성 검정 알고리즘을 수행하는 단계를 포함하여 이루어지는 것을 특징으로 하는 유한 오토마타 기반의 프로토콜 명세에 대한 검정 방법
|
| 10 |
10
제 9 항에 있어서, 상기 블럭 초기화 과정은 오토마타 사용자로부터 키보드로 행위1, 행위2, 행위3을 차례로 입력받아 상태 도달성에 해당하는 논리식에 따라 맥스 블럭과 민 블럭으로 나누어 해당 변수를 생성하는 것을 특징으로 하는 유한 오토마타 기반의 프로토콜 명세에 대한 검정 방법
|
| 11 |
11
오토마타 모델내에 어떠한 천이도 존재하지 않는 deadlock 상태와 상태의 부분집합만을 무한히 반복하여 초기상태로 돌아가지 못하는 livelock 상태 혹은 상태집합이 존재하는지를 검사하는 안전성 검정 과정과, 상기 오토마타 모델의 임의의 상태에서 같은 행위에 의한 둘 이상의 천이가 존재하는 비결정성을 검정하는 결정성 검정 과정과, 상기 오토마타 모델 내의 임의의 상태에서 입력 행위와 출력 행위의 발생여부를 검사하는 상태도달성 검정을 위하여 Modal mu-calculus의 논리식으로 표현된 상태도달성 특성을 오토마타가 만족하는지를 모형 검사의 기법을 통하여 확인하는 상태도달성 검정 과정과, 상기 오토마타 모델에서 연속적인 세가지 행위가 명세내에서 과연 발생하는지를 검사하는 행위도달성 검정을 위하여 Modal mu-calculus의 논리식으로 표현된 행위도달성 특성을 오토마타가 만족하는지를 모형 검사의 기법을 통하여 확인하는 상태도달성 검정 과정을 실행시키기 위한 프로그램을 기록한 컴퓨터로 읽을 수 있는 기록매체
|
