Esterel을 위한 오토마타 생성 기반구조

Abstract

반응형 시스템은 물리적 환경과의 소통을 하는 항공기 제어 시스템, 자동차 제어 시스템과 같은 제어 시스템에 내장이 되어 사용된다. 이러한 반응형 시스템은 내부 시스템과 외부 환경과의 소통을 통해서 이벤트가 발생하기 때문에 안전성에 매우 민감하다. 때문에 반응형 시스템에 대한 안전성 검증 및 테스팅과 같은 수행이 꼭 필요하다. Esterel 언어는 INRIA에서 Gerard Berry에 의해서 개발된 반응형 동기식 언어이다. 실제로 다양한 기계에 내장이 되는 제어 시스템 개발에 널리 이용되고 있다. Esterel은 동기식 언어로 실제 시간을 논리적 시간 단위 (instant)로 나누어 시스템 시간을 제어하고 있다. 실제 하드웨어와 유사하게 한 단위 시간 내에서 입력 시그널이 켜짐 상태로 바뀌는 즉시 출력 시그널의 상태가 켜짐 상태로 바뀌게 된다. 이러한 상태는 그 단위 시간 내에서만 유효하고 다음 단위 시간으로 바뀌게 되면 상태는 초기화 된다. 이러한 하드웨어와 유사하게 작동하는 특징은 반응형 시스템 개발을 보다 쉽고 간편하게 수행될 수 있도록 한다. 다른 중요한 특징으로 Esterel 언어는 유한 상태 기계 (Finite State Machine)과 동일한 정형적 의미를 가진다. 즉, Esterel 프로그램의 의미는 오토마타와 동일한 의미를 가진다. 이 특성은 Esterel 프로그램에 대한 분석에 유용한 분석 방법을 제공하며, 안전성에 대한 검증 및 테스팅을 수행하는데 있어서 유용하게 사용될 수 있다. 따라서 이러한 특성을 이용하기 위해서는 Esterel 프로그램으로부터 오토마타 생성이 필요하다. 생성된 오토마타는 다양한 오토마타 이론의 적용이 가능하고, 모델 체킹과 같은 다양한 분석에도 활용될 수 있다. 본 논문에서는 Esterel을 위한 Esterel 문법 구조 바탕의 오토마타 생성 규칙을 제안한다. 제안된 오토마타 생성 규칙은 다양한 분석에 유연하게 이용될 수 있다. 이 생성 규칙을 바탕으로 Esterel 프로그램으로부터 오토마타를 생성하기 위한 오토마타 생성 기반구조를 설계하였다. 우리의 생성 기반구조는 오토마타 생성과 더불어 이를 사용자가 생성된 오토마타를 이미지 형태로 관찰 할 수 있도록 출력한다. 특히 우리의 생성 기반구조는 사용자의 관심 대상을 입력으로 받아 이에 대한 오토마타만을 생성하도록 한다. 이는 전체 오토마타에서 사용자의 관심 대상 오토마타 상태만을 관찰할 수 있게 함으로써 오토마타의 활용도와 오토마타를 대상의 분석을 수행함에 있어서 효율성을 높이기 위함이다. 본 논문에서는 관심 대상을 출력 시그널에 초점을 맞추어 다루었다. 신호등 제어 시스템을 대상으로 오토마타 생성 기반구조에 대한 실험을 진행하였고, 실험을 통해서 전체 오토마타와 관심 대상 오토마타를 얻었다. 얻어진 실험 결과를 통해서 관심 대상 오토마타가 전체 오토마타에 비해서 많은 간선과 노드를 줄일 수 있음을 보일 수 있었다. 이를 통해서 우리가 제안하는 생성 규칙이 실제 분석에서 사용될 수 있음을 보였고, 또한 우리의 생성 기반 구조가 효과적으로 검증 및 테스팅 수행에 도움이 될 수 있음을 알 수 있었다.