Model verification examines the correctness of a model implementation with respect to a model specification. The model specification describes not only behavioral but also structural properties of a real system to be modeled. While described from model specification, implementation prepares to execute and
evaluate a simulation model. Therefore, various implementation test methods have been evaluated for several years, especially within protocol conformance test and software test. Simulation model verification is experimented among various implementation tests. While former studies have merely focused on finite state machine(FSM), a simulation model usually consists of structural and behavioral properties with time constraints and finite states. However, it is difficult and complex to ensure the correctness of such a time constrained finite state implementation. In order to overcome the complexity of the problem, this paper presents a new method that provides the time constrained simulation model verification. The objective of this verification is to inspect the ways in which implementation satisfies specification at I/O level, not verifying whether implementation works exactly the same as specification. Implementation has I/O function level system morphism from specification, i.e., implementation accepts all possible I/O sequences that specification specifies. Timed state reachability graph(TSRG) is devised to generate all possible I/O sequences from a given DES model. Time complexity of all possible I/O sequences is too high to apply in practical test. To solve such time complexity, this paper proposes a method to reduce the redundancy of all possible I/O sequences, called a test I/O sequences set. Model verification can find all implementation faults by using the test set under the assumption that the maximum state size of the test target can be known. This assumption helps to find faults of the test target in a practical time bound. Time complexity of the proposed method shows O(N * E), which is superior to compared with the timed Wp method.
To build an automatic verification environment, modeling language is required at a front-end of the environment. This paper proposes a DEVS (Discrete Event Systems Specification) modeling language, called DEVSpecL (DEVS Specification Language). DEVSpecL is a basis for modeling, simulation and analysis within a DEVS based framework for seamless systems design. Models specified in DEVSpecL can be translated in different forms of codes by code generators, which are executed with various tools for models verification, logical analysis, performance evaluation, and others. The implementation of the proposed approach requires a DEVS interface to communicate with various simulation engines. The interface deals with only a timer and I/O events. The whole verification process has three steps such as a TSRG model generation from a DEVSpecL model, a test I/O sequences set generation from the TSRG, and model verification using the test set under system morphism at an I/O function level. The implementation of the proposed approach shows 100\% coverage of faults through a verification of an assembly line model implemented in three world views: event-oriented, process-oriented, and object-oriented approaches. For an application of TSRG, this paper proposes a method for testing of message loss by means of Linear Programming technique. In the application, DEVS formalism is employed for discrete event modeling in which communication between atomic models relies on weak synchronization. Timed state reachability graph is first employed to generate all possible timed event sequences from DEVS models, which are then transformed into a set of time constraint equations. Finally, message loss between communicating discrete event models is tested by solving such equations using LP technique.
모델 검증은 모델규격에대해서 그 모델의 구현의 정확성을 검사하는 것이다. 모델규격은 실제시스템의 행동양식 뿐 아니라 구조적인 특성들에대해서도 기술하는데 반해, 구현은 모델규격을 시뮬레이션 프로그램화 하는것이다. 수년간 다양한 구현 검증 방법들, 특히, 프로토콜 검증분야와 소프트웨어 검증분야에서 개발되고 평가되었는데, 시뮬레이션 모델검증 또한, 그러한 분야중 하나이다. 이전의 연구들은 주로 유한 상태 기계(FSM)에 촛점을 맞춘반면, 시뮬레이션 모델은 일반적으로 구조적 특성과 시간제한과 유한상태적인 행동양식을 가진다. 그러나, 시간제한적 유한상태 구현의 정확성을 보장하는것에는
복잡성과 어려움이 존재한다. 그러한 복잡성의 문제를 극복하기 위해, 본논문에서는 시간제한적 시뮬레이션 모델 검증을 위한 새로운 방법을 제안하는 바이다. 이 검증의 목적은 구현이 규격과 정확히 같은것이냐를 보는것이 아니라 구현이 규격을 I/O 수준에서
만족하는지를 검사하는 것이다. 이것은 구현이 규격에대해서 I/O 함수 시스템 사상성을 가진다는 의미, 즉, 구현이 규격에서 제안하는 모든가능한 I/O 순서들을 다 만족한다는 의미를 지닌다. 시간상태도달 그래프 (TSRG)는 다양한 이산사건시스템 모델들로 부터 쉽게 모든 가능한 I/O 순서들을 얻기위하여 고안되었다. 모든 가능한 I/O 순서들은 실용적 관점에서 매우 높은 시간복잡도를 가진다. 그러한 시간 복잡도를 해결하기위해, 본논문은 모든가능한 I/O 순서들에서 불필요한 것들을 제거하는 방법을 제안한다. 줄어든 I/O 순서들은 테스트 I/O 순서의 셋이라 하는데, 모델 검증이 실용적 시간내에 수행되기 위해 검증대상 상태의 최대값은 알고 있는 가정하에서 테스트 셋을 이용하여 모든 구현 오류들을 발견할 수 있다. 제안된 방법의 시간 복잡도는 O(N * E) 로써 이것은 timed Wp 방법과 비교하여 우월한 성능을 보인다.
자동화된 검증환경을 구축하기 위해, 모델링 언어가 환경의 앞단으로써 필요하게 되는데, 본 논문은 DEVS 모델링 언어로써 이산사건 시스템을 DEVS 기반의 프레임웍상에서 끊임없는 시스템 설계를 할수있도록 모델링, 시뮬레이션, 분석하는데 기반이되는 DEVSpecL이라고 불리는 모델규격언어를 제안한다. DEVSpecL로 기술된 모델들은 코드생성기에
의하여 다른 형태의 코드들로 번역이 될수 있다. 그것들은 모델 검증, 논리 분석, 성과 분석, 등등의 다양한 도구들과 함께 수행될수 있다. 제안된 방법론의 구현은 다양한 시뮬레이션 엔진들과 교류하기위해 타이머와 I/O사건들만 다루는 DEVS 인터페이스를 요구한다. 전체 제어 과정은 세단계로 이루어지는데, DEVSpecL모델에서 TSRG 모델 생성단계,
생성된 TSRG모델로부터 테스트 셋 생성단계, I/O 수준 시스템 사상성하에서 테스트 셋을 이용한 모델검증단계로 이루어진다. 제안된 방법론은 세가지 세계관(world view), 즉, 사건지향형, 프로세스지향형, 개체지향형 방법들로 구현한 조립공정의 검증을
통해서 모든 오류를 검증할수있음을 보인다. 그리고, TSRG의 응용으로써, 본 논문은 검증방법론의 응용예로써 선형계획법을 이용한 메시지손실의 검사 방법을 제안한다. DEVS 형식론은 atomic 모델, 즉, 가장작은 모델들 사이의 약한 동기화를 이용한 통신을 하는
이산사건모델링방법론이다. 시간상태도달그래프가 DEVS 모델들로 부터 모든 가능한 시간사건연속물들을 발생시키기 위하여 고안된것이다. 그것은 시간제한식들로 변한되어지고, 이산사건 시스템 모델들간의 메시지손실은 선형계획법을 이용하여 시간제한식들을 풀어냄으로써 계산되어질수있다.
