초록 close

본 논문에서는 모델 체킹을 시스템의 성능상의 효율성 분석에 적용하는 방법에 대해 논한다. 시뮬레이션이나 실험적인 측정을 통해 시스템의 성능저하를 찾는 것은 쉽지만, 성능을 저하시키는 요인을 분석해 내는 것은 사실상 매우 어렵다. 특히, 시스템 자체가 매우 복잡해지고, 주위 다른 시스템과의 상호 동작을 하게 되면 소스코드의 분석을 통한 오류 발견은 거의 불가능해진다. 이에 본 논문에서는 모델 체킹에 사용되는 시제논리를 통해 시스템의 자원 활용도를 명세하고, 이를 이용해서 모델 체킹을 수행함으로써 성능 저하를 발생시키는 요인을 찾아내는 방법에 대해 논한다.


This paper addresses how model checking methods can be applied to utilization analysis of system. Measuring a system performance using simulation is an easy task but finding the bottleneck in a certain system is not an easy task. Especially, system is getting complicated and interacts with other systems, which makes the analysis very difficult. As an alternative approach, we show that can specify system utilization properties using temporal logic, and can find a reason of a system performance drop easily using model checking.