Maude를 통한 분산 드론 시스템의 정형 분석

Abstract

사이버 물리 시스템(CPS)은 물리적 컴포넌트와 소프트웨어 컴포넌트가 통합된 분산 시스템으로 여러 산업 분야에서 널리 사용된다. CPS는 분산 환경에서 실시간으로 정보를 교류하며, 실제로는 여러 시간 오차 때문에 비동기적으로 동작하지만 전체는 논리적으로 동작한다. 실시간 분산 시스템의 물리적 컴포넌트 등과 같은 CPS의 복잡성으로 인해 이를 분석하고 검증하는 것은 매우 어려운 일이다. 이 연구에서는 여러 대의 드론으로 이루어진 시스템의 분산 합의 알고리즘을 정형 기법을 통해 명세하고, 시뮬레이션 및 상태 공간 탐색 등 여러 정형 기법을 이용하여 분산 드론 CPS이 만족해야 하는 요구 사항에 대한 검증을 진행하였다.