A complete and consistent specification is essential in software development to improve productivity, software reliability, and maintainability.
In this thesis, a verification system which combines verification with AI techniques and generates rather consistent and complete S/W specification is implemented. For this purpose, this thesis uses first order predicates logic for representation of specification, because through the use of first order predicates logic, analyst can verify specification more conveniently, prudently, and methodology-independently. As a prototype, this thesis implements a verification system which converts the specifications in PSL to logic facts in prolog and validates them.
소프트 웨어 개발과정중 초기 단계인 명세 단계에서 생기는 실수는 소프트 웨어 개발 비용에 큰 영향을 초래 한다. 또한 소프트 웨어 자체의 생산성 (productivity) 과 안전성 (reliability) 그리고 유지 가능성 (maintainability) 을 증진시킨다는 관점에서 볼때 완전성 (completeness) 과 일관성 (consistency) 을 가지는 명세서의 개발은 매우 중요하다.
본 논문은 완전성과 일관성을 가지는 명세서의 개발을 지원해주는 지식 기반의 검증 시스템 (knowledge based verification system;KBVS)의 구현을 목적으로 하고있다. 이를 위해 지식 표현으로 일차 술어 논리 (first order predicates logic) 를 사용 한다.
지식 기반의 검증 시스템은 특정분야의 전문 지식 (domain knowledge) 을 통하여 종전의 시스템 보다 더욱 의미적인 검증 (semantic verification) 을 가능케 하고, 사용자의 의견을 더많이 수렴하여 명세서에 사용자의 요구를 충분히 반영할 수 있도록 도와준다. 또한 정적, 동적인 측면을 동시에 고려한 검증을 가능케하며, 서로 다른 방법론을 따라서 기술된 명세서도 검증 할수 있게 지원 해 준다.
본 논문은 이러한 목적의 원형예로써 PSL(problem statement language) 로 기술된 명세서를 입력하여 이를 일차 술어 논리로 바꾼후 검증을 해주는 시스템을 구현하고 있다.
