Many modern systems show dynamic characteristics in a sense that they change their configuration dynamically during run-time. In object-oriented systems, for example, the configuration of objects and their links change to reflect the state of such systems. Unfortunately, few analysis techniques address the dynamic nature explicitly. Most of them abstract away the dynamic nature of systems. Thus, there is a gap between analysis result and the reality.
The goal of this dissertation is to propose a specification and validation technique for dynamic systems. In particular, we note that there exist few researches on the property specification of dynamic systems. We propose a new temporal logic, called HDTL, for specifying the required property. By employing the notion of freeze quantifier, HDTL allows us to specify the correctness requirements of dynamic systems precisely.
We suggest two analysis methods for HDTL. The first is trace checking which automatically analyzes whether an execution trace generated from a system is consistent with a specification written in HDTL. We show the experiments using two different languages; SDL, an international standard modeling language for communication systems, and Java, an implementation language.
The second analysis is model checking. The behavior model of a system is described in Maude, a formal method tool that supports modeling of con-current object-oriented systems. We show how to perform model checking using the HDTL checker, originally developed for trace checking. The fact that HDTL specification can be used both in the trace checking, and in the model checking shows that HDTL specification is reusable. A model with relatively lower complexity can be model-checked with an HDTL formula. After refinement, the same formula can be used to validate the refined model or the implementation, by trace checking.
많은 시스템들은 그 구성이 수행시간 중에 동적으로 변하는 특징을 가지고 있다. 예를 들어 객체 지향 시스템의 경우, 시스템을 구성하는 객체들과 그들 사이의 연결은 동적으로 생성, 삭제된다. 하지만 대부분의 기존 분석방법들은 그러한 특징들을 추상화시켜, 정적인 구조를 가지는 것으로 가정하고 분석하기 때문에, 분석결과와 시스템의 실재 사이에 차이가 존재하게 된다. 따라서 이러한 정보의 손실없이 동적 시스템의 특징을 분석하는 기법이 필요하게 된다.
이 논문에서는 이러한 동적 시스템의 명세 및 검증 기법을 제안하였다. 우리는 병렬 시스템의 명세에 많이 사용되는 시제논리를 확장하여 HDTL이라는 명세언어를 제안하였다. 우리는 동결 한정자(freeze quantifier)라는 개념을 사용함으로써, 동적 시스템의 특성명세를 정확히 기술할 수 있도록 하였다.
HDTL을 사용하는 분석기법의 예로서, 우리는 두가지 기법을 제안한다. 첫 기법은, 시스템이 수행되었을때 생기는 수행결과를 HDTL 요구명세와 비교하여 분석하는, 동적 분석(dynamic analysis) 기법이다. 수행결과가 HDTL 요구명세와 어긋나는 경우, 이 알고리즘은 문제에 관련된 이벤트들을 출력하여, 문제의 원인을 발견하는데 도움을 주게 된다. 이를 위해 우리는 rewrite logic system인 Maude를 이용하여 HDTL을 위한 동적 분석 알고리즘을 구현하였다. 이 알고리즘의 적용 예로서, 우리는 2가지 동작 기술 언어를 사용한 실험을 통해 적용성을 보였다. 첫째는 통신 시스템 기술을 위한 국제 표준 언어인 SDL이고, 둘째는 병렬 객체지향 구현 언어인 Java 이다.
또 한가지 분석 기법은 모델체킹이다. 이는 하나의 수행결과가 아닌, 시스템의 동작 모델 자체와 HDTL을 비교하여 분석하는 기법이다. 이때 시스템의 동작 모델은 Maude로 기술되며, 동시에 그 동작 모델이 HDTL 명세와 일치하게 수행되는지를 검사하는 감시자(observer)를 HDTL에서 자동으로 생성하게 된다. 이 두 모델을 병렬로 수행시키고, 그때의 상태공간을 탐색해 봄으로써, 우리는 동작모델에 존재하는 HDTL 명세와의 불일치를 찾아낼 수 있다. 우리는 에이전트 기반 시스템의 동작을 모델링하고 검증해 봄으로써, 이 기법의 적용성을 확인할 수 있었다.
