| 摘要 |
<p>본 발명은 모델 검사용 동작 환경을 자동적으로 생성하는 방법에 관한 것이다. 디자인의 시뮬레이션 중 포착된 상태 천이에 대하여 모델 검사를 사용함으로써 테스트중인 디자인의 검증을 자동적으로 향상시키는 방법이 제공된다. 포착된 모든 개별 천이가 시뮬레이션 중 사용되지만, 이들 천이의 모든 가능한 시퀀스가 반드시 시뮬레이션 중 사용되지는 않고, 이 사용되지 않은 시퀀스에 버그가 숨겨져 있을 수 있기 때문에 향상된 검증이 가능하다. 모델 검사기의 비결정적이며 철저한 특성에 의하여 포착된 상태 천이로 이루어지는 모든 가능한 시퀀스가 사용되는 것이 보장된다. 본 발명의 방법은 상태 천이의 활용과 이들 상태 천이(시뮬레이션중 관측됨)를 유발하는 입력으로 구성되어, 모델 검사기가 테스트중인 디자인에 인가될 수 있는 올바른 입력을 비결정적이며 철저하게 정의한다.</p> |
