Recently, software systems have become increasingly concurrent and distributed, and it has become highly important to model and analyze the interactions in the message-based communication systems based on scenario specifications. The major concern when developing the systems using scenario specifications is the possibility of unexpected behaviors which is known as emergent behavior. The emergent behavior arises because specifications can be interpreted in various ways due to the different perspective of a reader or the lack of the information in the specifications. Thus, the scenario specifications should be verified to fix or elaborate the faulty specifications before implementing the system. Most previous studies on the verification used the model-checking technique using the state machine as a behavioral model. However, this model often faces the state explosion problem, which occurs with the growth of the number of states in asynchronous communications. In this paper, we provide the verification technique to fix the potential problems of emergent behaviors in scenario specifications by using the partial order-based approach. Based on the partial order extended to model the exclusive-or(XOR) branches, the size of the analyzed state space can be reduced, which avoids the state explosion problem, and thus the detection process can be performed efficiently. 16 resolving patterns are suggested to support the automated resolving process for fixing causes of the emergent behaviors. We evaluated our approach on the contracts of Singularity operating system developed by Microsoft Research. Three violated relations are detected and the corresponding emergent behaviors are correctly disappeared. In addition, we showed that as the system becomes larger and uses asynchronous communications, the efficiency of our approach for modeling and analyzing of scenario specifications is increased.
최근에 소프트웨어 시스템은 점점 더 동시성을 갖는 분산화된 시스템이 되고 있어서, 메시지 기반 통신 시스템에서의 상호 작용을 모델링하고 분석하는 것이 매우 중요해 지고 있다. 이런 메시지 기반 통신 시스템은 일반적으로 시나리오 명세 형태로 전체 시스템에 대해 설계되고, 여기에 명시된 협업 구조를 따라 각각의 서브 시스템들이 상세 설계된다. 시나리오 명세를 사용하여 전체 시스템을 설계할 때 중요한 고려 요소는 돌발 행위로 알려진 예상치 못한 행동이 일어날 가능성이 있는지 확인하는 것이다. 읽는 사람의 관점 차이나, 특정 정보의 부족으로 인해 시나리오 명세를 다양한 방식으로 해석할 수 있는 경우 돌발 행위가 발생한다. 따라서 시스템을 구현하기 전에 시나리오 명세를 검증하고, 오류가 있거나 해석의 다양성이 있는 부분을 수정해야 한다. 대부분의 이전 연구들은 상태 머신을 행동 모델로 사용하는 모델 검사 기법을 사용하였는데, 이러한 경우 종종 비동기 통신의 상태 수가 증가함에 따라 발생하는 상태 폭발이 일어날 수 있다. 이러한 문제를 해결 하기 위해, 이 논문에서는 Partial Order에 기반한 기법을 사용하여 시나리오 명세에서 나타나는 돌발 행위의 잠재적 문제를 제거하는 검증 기법을 제안한다. XOR 분기를 모델링하기 위해 확장된 Partial Order 모델에 기반하여, 분석 시에 상태 공간의 크기를 줄일 수 있고, 비동기 통신에서도 상태 폭발을 피할 수 있으며, 검출 프로세스가 효율적으로 수행 될 수 있다. 또한 돌발 행위를 자동화된 방법을 통해 제거하기 위해, 다양한 제약 조건을 고려한 제거 패턴들을 제안한다. 기법에 대한 검증을 위해, Microsoft Research에서 개발한 Singularity 운영 체제에서 사용하는 Contract들에 본 기법을 적용하였다. 세 가지 위반 관계가 발견되었고, 자동화된 제거 기법에 따라 발견된 돌발 행위가 올바르게 제거되었다. 또한, 시스템이 커지고 비동기식 통신을 사용함에 따라 동시성이 커질 수록 시나리오 명세 모델링 및 분석을 위한 본 기법의 효율성이 증가한다는 것을 실험을 통해 확인하였다.