검증에 사용하는 명세는 대부분 1차 술어 논리(First Order Logic)로 이루어져 있다. 1차 술어 논리가 자연언어 대부분을 표현하지만 표현하지 못하는 부분도 존재한다. 이를 해결하기위해 양상논리(Modal Logic)를 추가한 명세방법이 존재하지만 간접적인 방법으로만 존재할 뿐 이다. 본 논문에서는, 양상논리를 이용한 명세의 직접적인 표현을 위해 BML(Bytecode Modeling Language)을 확장한다. 이를 통해, 명세정보 표현의 정확성을 향상시킨다.
