Statecharts is a visual specification language widely used for specifying requirements of reactive system. The expressive power of Statecharts with features such as parallelism and hierarchy of statecharts makes it suitable for specifying large and complex systems. Analysis techniques like model checking facilitate to analyze the statecharts, but, unfortunately, suffer from the state-explosion problem. Therefore various techniques have been developed to cope with this problem. Among them, module-based assume-guarantee reasoning is adopted in our work to deal with this problem for the statecharts.
For assume-guarantee reasoning, notions of modules, assumptions and guarantees are needed. Definition of modules in the statecharts includes notions of event scoping and assumptions about the environment. Using the statecharts module, we have designed an algorithms to make a guarantee of it under the given assumptions. To make a guarantee, we define a macro step model of the statecharts modules, and with this guarantee, a reduced macro step model is developed. We have conducted an empirical study with an example, Coffee Vending Machine, using the verification framework proposed by O. Grumberg et al[1]. As a result, we obtained reduced complexity, and further more we found the effectiveness of our method in the case of many internal states.
Statecharts는 병렬성(parallelism), 계층성(hierarchy), 브로드케스팅(broadcasting)을 포함하는 상태 다이어그램(State Diagram)으로 리액티브 시스템(Reactive System)의 명세에 많이 사용되는 명세 언어이다. 모델 체킹(Model checking)과 같은 분석 기법이 Statecharts에 적용되면서 자동화 된 시스템 검증이 용이하게 되었으나, 모델 체킹을 이용한 검증은 상태 폭발 문제(State-explosion problem)를 피할 수 없기 때문에 모델 체킹을 이용한 Statecharts 검증 또한 이 문제를 가지고 있다. 본 논문에서는 모듈 기반의 가정-보증 추론(Assume-guarantee Reasoning)을 이용하여 Statecharts에서 발생하는 상태 폭발 문제를 해결해 보고자 한다.
가정-보증 추론은 모듈 및 가정, 보증의 개념을 갖고 있으므로, 이 방법을 이용하여 Statecharts를 검증하기 위해 우선 모듈의 개념을 정의하였다. Statecharts 모듈은 이벤트 스코핑(Event scoping)과 환경에 대한 가정을 포함한다. 이 Statecharts 모듈 정의을 이용하여 보증을 끌어내기 위해 본 연구에서는 매크로 스텝 모델(Macro-step Model)을 정의하고 모델을 이끌어내는 알고리즘을 제안하였다.
커피 자판기 예제를 사용하여 본 연구에서 제안한 방법을 수행해 보았다. 그 결과 일반적으로 제안한 방법을 사용하는 경우, 검증의 복잡도가 감소함을 알 수 있었고, 특히 사용되는 모듈이 많은 내부 상태(internal states)를 가지고 있는 경우에는 큰 효과를 나타냄을 알 수 있었다.
