Bisimulation has been used as a logical verification method for the algebra-based formalisms such as CCS and CSP. It is an equivalence concept between two systems. The fact that two systems are bisimilar means that their I/O behaviors are same. If any event sequence can be observed from one system, then the same event sequence should be observed from the other system too.
Though Bisimulation is a powerful and generally used verification method, there is a big problem, 'State Explosion'. If a system becomes larger than a specific limit, the state space of the system increases explosively and makes verification beyond the computational power. This is the main reason why the bisimulation method is not used widespread in the real industry. There have been several approaches to solve this problem and still being researched. This thesis proposes a hierarchical bisimulation as a solution for the state explosion.
The hierarchical bisimulation takes the divide-and-conquer approach. Trying to compute the overall verification at once results in the state explosion. If the verification can be divided into several parts and computed part-by-part, the state explosion won't happen. DEVS formalism supports this approach. DEVS formalism describes a system in a hierarchical and modular style, which the hierarchical bisimulation takes advantage of. The hierarchical bisimulation is an equivalence relation between two systems with respect to the overall hierarchy and component modules. If the overall hierarchy is preserved the module-by-module verification guarantees the overall equivalence, which means that the overall verification can be divided into several module-by-module verification and the state explosion problem can be solved.
This thesis proposes several frameworks that support the hierarchical bisimulation. We propose two formalisms based on the DEVS formalism as modeling methodologies and present two equivalence concepts for the proposed formalisms. Last, we propose a system development and verification framework in which a system can be developed in a top-down and stepwise style and verified by the hierarchical bisimulation without the state explosion.
Bismulation 기법은 CCS나 CSP등의 형식론에 적용된 시스템 검증 기법중 하나이다. 이는 두 시스템간의 입출력 관점에서 등가 개념이다. 만약 한 시스템에서 특정한 일련의 사건들이 관찰된다면, Bisimulation 관계에 있는 다른 시스템에서도 역시 같은 사건들이 같은 순서로 관찰되어야만 한다.
Bisimulation이 효과적이고 또 널리 쓰이는 검증 기법이긴 하지만 상태 폭발이란 큰 문제점을 안고 있다. 만약 시스템의 규모가 어느 한계 이상으로 커진다면 시스템의 상태 공간은 폭발적으로 증가하여 계산 능력의 한계를 벗어나게 된다. 이는 정형 검증 기법이 실제 산업계에서 널리 사용되지 못하고 있는 이유이기도 하다. 이 문제를 해결하기 위하여 여러 가지 시도가 있었다. 본 논문에서는 계층적 Bisimulation 기법을 해결책으로 제시한다.
계층적 Bisimulation 기법은 'Divide-and-Conquer' 접근 방법을 따른다. 시스템 전체에 대한 검증을 한꺼번에 수행하려 하는 것은 상태 폭발을 야기한다. 만약 전체 검증 과정이 여러 개의 작은 부-검증 과정으로 나뉘어 계산될 수 있다면 상태 폭발은 발생하지 않는다. DEVS 형식론은 이러한 접근 방법을 지원한다. DEVS 형식론은 시스템을 계층적으로 기술한다. 계층적 Bisimulation은 시스템의 두 측면, 즉 계층적 구조와 모듈별 등가성을 검증한다. 만약 계층적 구조가 보존된다면 모듈별 등가성 검증만으로 전체 시스템을 검증할 수 있다. 즉 전체 시스템 검증 과정을 여러 개의 모듈별 등가성 검증으로 나눌 수 있다. 이는 상태 폭발 문제를 해결할 수 있음을 의미한다.
본 논문은 계층적 Bisimulation을 지원하기 위한 틀을 제안하고 그 효용성을 증명한다. 'Top-Down' 접근 방법으로써 상태 폭발 없이 단계별로 시스템을 개발하고 검증할 수 있는 시스템 개발 및 검증 방법론을 제안하고 기존의 방법과 비교하였다.
