병행적 유한상태머신의 상태폭발 완화를 위한 병렬적 상태 공간 순회 기법 = State Space Parallel Exploration of Concurrent Finite State Machines for reducing State Space Explosion

다국어 초록 (Multilingual Abstract)

In model driven engineering, formal model is developed then refined, and transformed to source codes. In this approach, model based verification is performed to test the system rather than code based verification. Generally, behaviors of the system are described by state-based formal modeling language such as UML state machine, Petri nets or FSM(Finite State Machine). In most cases, behavioral model of the system is transformed to FSM models due to its simple structure. In this reason, FSM based state space exploration technique is important to verify system behavior. However, there is the state explosion problem that the state space is too big to explore when the system is getting bigger and more complex. To reduce this problem, there are many studies for parallel state space exploration with efficient state space partitioning technique but there is still a similar problem in each processor. In this paper, a new approach is provided to reduce the problem in each processor for parallel state space exploration. This approach focuses on providing efficient exploration techniques in each processor instead of making a good partitioning function. And experimental results will be shown to prove these techniques making the parallel state space exploration fast.

목차 (Table of Contents)

• 제 1 장 서론 1
• 제 2 장 연구 배경 4
• 2.1 유한상태머신과 병행적 합성 4
• 2.2 유한상태머신의 순회 7
• 2.3 유한상태머신의 병렬적 순회 8
• 2.4 관련연구 10
• 제 3 장 상태폭발 문제 해결 방안 13
• 3.1 유한상태머신의 병행적 순회 기법 13
• 3.2 부분 방문 기록 기법 15
• 3.3 개선된 병렬적 유한상태머신 순회 방법 17
• 제 4 장 기존 방식과의 효율성 비교 22
• 4.1 공간적 상태폭발의 완화 24
• 4.2 시간적 상태폭발의 완화 25
• 4.3 병렬적 상태 공간 순회의 효율 개선 27
• 제 5 장 결론 32
• 참고 문헌 33