《과학연구부문에서는 나라의 경제발전과 인민생활향상에서 전망적으로 풀어야 할 문제들과 현실에서 제기되는 과학기술적문제들을 풀고 첨단을 돌파하여 지식경제건설의 지름길을 열어놓아야 합니다.》
UML설계의 정확성을 검증하기 위한 한가지 방안으로서 모형검사기술이 적극 리용되고있다.
모형검사기술은 주위환경과의 호상작용으로 특징지어지는 반작용체계의 정확성증명에 리용된다. 반작용체계들은 주위환경으로부터 입력을 받고 일정한 시간후에 입력에 대하여 응답하는 과정을 끊임없이 반복한다. 반작용체계의 실례로 조작체계, 비행기조종체계, 통신규약, 흐름조종쏘프트웨어 등을 들수 있다.
일반적으로 반작용체계는 매우 복잡하므로 그의 정확성을 검증하는것이 매우 중요하다.
모형검사의 기초원리는 콤퓨터에서 실행되는 검증알고리듬을 리용하여 체계의 정확성을 검증하는것이다. 사용자가 검증도구에 체계에 대한 모형과 요구사항을 입력하면 콤퓨터가 정확성을 증명한다. 만일 오유가 발견되면 검증도구는 어떤 조건에서 오유가 생길수 있는가를 보여주는 반례를 제시한다. 반례는 모형에 오유가 있으며 수정이 필요하다는것을 보여준다. 사용자는 모형검사를 하여 오유를 찾고 그에 따라 모형명세서를 수정한 다음 프로그람개발을 계속한다. 오유가 발견되지 않아도 사용자는 모형을 더욱 세련화시키고 다시 검증을 진행할수 있다.
모형검사를 위한 알고리듬은 구체적인 상태공간탐색에 기초하고있다. 모형의 매 상태에 대하여 그것이 정확히 동작하는가, 즉 상태가 요구하는 속성을 만족하는가를 검사한다.
모형검사알고리듬중에서 가장 간단한 형식은 도달가능성분석이다. 즉 체계가 전진이 더는 불가능한 어떤 상태(deadlock상태)에 이르는가를 판정하기 위하여 모든 도달가능한 상태들을 결정하고 더 이상 전진할수 없는 도달가능한 상태가 있는가를 판정한다. 도달가능성분석은 무한순환에 빠지지 않는다는것과 전체 실행과정에 성립하여야 할 불변속성을 증명하는데 적용할수 있다.
이와 같이 모형검사기술은 체계의 유한상태모형과 론리적속성이 주어졌을 때 그 속성이 주어진 모형에 대하여 성립하는가를 검사하는 기술이다.
모형검사기술을 실현한 도구들로서는 SPIN, SMV, UPPAAL등을 들수 있다.
체계의 모형을 모형검사도구들의 모형서술언어로 표현하는것은 전문가적인 지식을 요구하므로 체계의 모형을 UML로 작성하고 그것을 모형검사도구의 모형서술언어로 변환하여 UML설계의 정확성을 검증하기 위한 기술들이 연구되였다.
이러한 기술을 실현한 도구들로서 HUGO/RT, UML2PROMELA, UML2UPPAAL등이 있다. 이러한 도구들은 UML설계의 상태도와 협조도, 클라스도를 리용하여 모형서술언어를 생성하도록 설계하고 실현하였으며 여러 실례체계들에 대한 검증에 적용되여 효과성을 분석하였다.
현재 이러한 도구들이 여러가지가 나와있으나 UML설계도구들의 종류가 많은것으로 하여 입력에서 제한을 받고있으며 사용자의 측면에서 친숙한 환경을 제공해주지 못하고있다.
우리는 UML설계의 상태도와 활동도, 그리고 순차도에 대한 검증을 지원할수 있는 UML설계검증지원도구를 개발하였다.
우리가 개발한 도구는 EA(EnterpriseArchitectect)로 작성한 UML설계를 입력으로하고있으며 UML상태도와 활동도, 순차도에 대한 PROMELA언어를 생성하도록 설계하고 실현하였다.
상태도와 활동도에 대하여서는 SPIN의 뷰치(Buch)자동체에로의 변환리론을 리용하였으며 순차도에 대하여서는 통보문의 송수신사건을 리용하여 통보문의 발생을 표현하고 순차도의 연산자들에 대한 PROMELA언어를 생성하도록 하였다.
우리는 UML설계검증지원도구의 검증대상범위를 상태도와 활동도뿐만아니라 순차도에로 넓히였으며 사용자들이 검증지원도구를 쉽게 리용할수 있도록 편리한 대면부적인 환경을 실현하였다.
