Systems design has been an iterative process which involves several steps such as modelling, logical analysis, performance evaluation and implementation. If each step requires different model, it would be a major hurdle to a seamless design process. Therefore a unified modelling framework which provides a basis to specify models at different steps in common semantics is desirable. In this thesis we propose a new composition-based verification methodology for the DEVS (Discrete EVent Systems specification) models. The suggested composition-based technique is applicable not only to the formal verification area but also to the area of simulation-based verification. Therefore it provides an axis of a unified framework based on the DEVS formalism.
For the formal verification of discrete event systems we defined the CDEVS (Communicating Discrete Event Systems) formalism which is an extended version of the DEVS formalism providing the nondeterministic representation of a system. As a means of a systematic proof technique, two operations, namly composition and minimization, are defined. These operations are compatible with the meaning of the communication semantics of the DEVS models, thus they incorporate the feature of spontaneity of output events in an 10 (Input/Output) system. In our methodology, an implementation model is reduced to an observational equivalent model through a series of stepwise compositions and minimizations. This incremental approach alleviates the state explosion problem in a verification process. Once a final operational CDEVS model is obtained, it can be verified either by an equivalence checking algorithm or by a valid implementation relationship which investigates both the functional correctness and the timeliness property. The proposed approach is much promising when analyzing large systems. If a component should be changed due to a design error, the overall composed model can be rebuilt by just composing the changed model with the unchanged ones together.
Although the proposed method can partially solve the state explosion problem, it is still impractical to use the formal verification technique to real-world systems. In those cases, simulation is the only applicable method to verify such large systems. However simulation requires much computation power and time, which motivates us to develop a simulation speedup technique based on composition of simulation models. The technique may be viewed as a compiled simulation technique which eliminates the run-time interpretation of the communication paths between hierarchical DEVS models. The elimination has been done by a behavior-preserved transformation method based on the closure under coupling property in DEVS theory. Experimental results show that the simulation speed of the composed DEVS models is about five times faster than that of the original ones. As the method was defined in a formal way it was easily implemented as an automated tool. In fact, the tool could always benefit the multi-component DEVS models to be simulated faster.
시스템 디자인 과정은 모델링, 논리적 해석, 성능평가, 구현 등의 여러 단계로 구성된다. 만일 각각의 단계에서 서로 다른 모델이 사용되어져야 한다면 매 단계마다 별도의 모델을 만들고 그 유효성을 따져야 하는 과정이 추가로 요구된다. 이러한 이유때문에 모든 단계에서 동일한 모델을 적용하여 작업할 수 있는 통합된 틀을 구축하는 것이 필요하다. DEVS (Discrete Event Systems Specification) 모델은 시뮬레이션을 위해 개발된 모델이지만, 시스템의 행위를 정형화하여 나타낼 수 있으므로 논리적 해석 과정에서도 사용되어 질 수 있다. 본 논문에서는 모델 복합법(Composition)에 기반한 DEVS 모델의 검증 방법론을 제안한다. 제안한 방법론은 DEVS모델의 논리적 해석 작업을 가능하게 함으로써 DEVS에 기반한 통합된 시스템 개발 틀의 한 축을 이룰 수 있기 때문에 그 의의가 크다.
먼저, 시스템의 정형적 검증(Formal Verification)을 위해 기존 DEVS 모델을 확장하여 CDEVS (Communicating DEVS) 모델을 제안하였으며, 논리적 검증 방법론을 위해 모델 복합법과 모델 축소법 (Minimization)의 두 연산을 정의하였다. 시스템의 행위를 CDEVS로 모델링하고, 검증하고자 하는 특성을 또다른 CDEVS인 스펙 모델로 기술하면, 위 두 연산을 단계적으로 적용하여 입출력이 같으나 축소된 형태의 검증용 모델을 구할 수 있다. 검증용 모델은 입출력 사건의 동일 관측성 관계(Input/Output Observational Equivalence Relation)를 기준으로 스펙과 일치하는지 그 여부를 확인할 수 있다.
정형적 검증 방법론은 신뢰성을 완벽히 보장해 줄 수 있으나, 대상 시스템이 복잡해짐에 따라 전체 상태수가 폭주하게 되어 적용이 불가능해지는 단점이 있다. 이러한 경우에는 시뮬레이션 기반 검증법이 적용될 수 있는데, 이 기법에는 시뮬레이션 시간이 많이 소요되는 문제점이 있다. 본 논문에서는 시뮬레이션 모델의 모델 복합법을 정의하고 적용하여 시뮬레이션 실행 속도를 개선할 수 있음을 보이고 있다. 제안한 방법은 번역 시뮬레이션 기술(Compiled Simulation Technique)의 일종이다. 시뮬레이션 속도 개선을 위해 시뮬레이션 실행 시간을 프로파일링(Profiling)하여 세 개의 부담(Overhead)으로 나누고 분석한 결과, 시뮬레이션 내부 메시지 패싱(Message Passing) 활동을 위해 가장 많은 시간이 소요된다는 것을 알 수 있었다. 메시지 패싱 활동을 없애기 위해 모델이 실행되기 이전에 모델을 번역하여 영향받는 부분들을 상호 합성해 줌으로써 실행 속도를 평균적으로 5배 이상 개선시킬 수 있었다.
