초록 열기/닫기 버튼
본 논문에서는 상호 작용 중심 시스템의 품질을 확보하기 위하여 LTL 분산 명세를 활용하는 연구를 소개한다. 이러한 시스템의 품질확보를 위해서는 모듈 간의 상호 작용을 확인하여 기대하는 요구 사항을 달성하고 있는지를 검사해야 한다. 이 작업은 어렵고 노동 집약적이며 전문가를 필요로 한다. 따라서 본 논문에서는 이 검사에 도움을 주기 위한 방법을 제안한다. 먼저, 시스템의 기대하는 요구 사항은 각모듈별로 분리해서 명세한다. 그리고 모듈 사이의 상호 작용은 다른 모듈이 수행하는 행위가 특정 모듈의 행위와 관련 있음을 의미한다. 여기서는 GR(1) 합성을 이용하여 명세를 만족하는 오토마타 모델이 생성되고 이것들은 소프트웨어 에이전트 기반의 시뮬레이터를 통해 모델의 행위를 확인하여 시스템이 요구 사항을 달성하고 있는지를 검사한다.
In this paper, we present a research utilizing decentralized LTL specifications for ensuring a quality for interaction-centralizedsystem. In this system, for ensuring the quality, we need to validate interactions between modules of the system and then we shouldcheck whether the system achieves the expected requirements. This task remains difficult and labor-intensive and requires an expert. In this paper, we present a method to assist such a task. First of all, the requirements of the system is written as multiple LTLspecifications. Interactions between modules mean that behaviors of one module are related with other one’s behavior. We generate theautomaton model fully achieving specification through GR(1) synthesis. And we simulate them using the simulator based on thesoftware agent for checking behaviors of the system. Finally, we validate the whole system whether it achieves given requirements.
키워드열기/닫기 버튼
Decentralized Specification, Generalized Reactivity(1) Synthesis, Simulation, Formal Method
