An reactive real-time system is embedded on control systems of machine like an airplane or automobile that have interaction with physical environment. An huge accident can be occurred from only small mistakes during the interaction. So needless to say, a program analysis and verification should be performed on these very sensitive control systems.
The Esterel Language developed by Gerard Berry in INRIA at France is widely used for programming synchronous reactive embedded systems. This synchronous language, Esterel, controls a time by dividing real time with logical time (instant) for synchronizing whole system with external clock. Reactive embedded systems can be simply designed by this features.
In addition, Esterel have a formal semantic structure based on a finite state machine that provide an efficient method to analyze program by static analysis. This property is very useful for verifying and testing safety-critical applications. For use of these feature, the method of the automata generation from Esterel program is required. The produced automata form translated from Esterel program can be utilized for model checking or applied with various automata theories.
In this thesis, we propose the automata generation rule for Esterel that reflects a structure of Esterel program and can be applied flexibly in various program analysis. The rule is based on Esterel`s syntax. Automata are produced by the automata generation framework we design and also user can observe the image form of produced automata. Notably, our framework produces parts of the whole automata that an user interest in. By doing so, the produced automata that an user want to observe in interest can improve utilization of automata and efficiency of an analysis for Esterel program. In this thesis, we target an output signal as our interest.
We experiment a traffic light control system by our framework. we get the two results from the system, one thing is the whole automata of the system, other thing is the part automata of the whole automata in our interest. The result show that our interested automata have a fewer edges and nodes in compare with the whole automata. From the experiments, we demonstrate that the automata generation rule can be applied flexibly in an analysis of Esterel program. And our automata framework can be facilitated for performing efficient verification or testing.
반응형 시스템은 물리적 환경과의 소통을 하는 항공기 제어 시스템, 자동차 제어 시스템과 같은 제어 시스템에 내장이 되어 사용된다. 이러한 반응형 시스템은 내부 시스템과 외부 환경과의 소통을 통해서 이벤트가 발생하기 때문에 안전성에 매우 민감하다. 때문에 반응형 시스템에 대한 안전성 검증 및 테스팅과 같은 수행이 꼭 필요하다.
Esterel 언어는 INRIA에서 Gerard Berry에 의해서 개발된 반응형 동기식 언어이다. 실제로 다양한 기계에 내장이 되는 제어 시스템 개발에 널리 이용되고 있다. Esterel은 동기식 언어로 실제 시간을 논리적 시간 단위 (instant)로 나누어 시스템 시간을 제어하고 있다. 실제 하드웨어와 유사하게 한 단위 시간 내에서 입력 시그널이 켜짐 상태로 바뀌는 즉시 출력 시그널의 상태가 켜짐 상태로 바뀌게 된다.
이러한 상태는 그 단위 시간 내에서만 유효하고 다음 단위 시간으로 바뀌게 되면 상태는 초기화 된다. 이러한 하드웨어와 유사하게 작동하는 특징은 반응형 시스템 개발을 보다 쉽고 간편하게 수행될 수 있도록 한다. 다른 중요한 특징으로 Esterel 언어는 유한 상태 기계 (Finite State Machine)과 동일한 정형적 의미를 가진다.
즉, Esterel 프로그램의 의미는 오토마타와 동일한 의미를 가진다. 이 특성은 Esterel 프로그램에 대한 분석에 유용한 분석 방법을 제공하며, 안전성에 대한 검증 및 테스팅을 수행하는데 있어서 유용하게 사용될 수 있다. 따라서 이러한 특성을 이용하기 위해서는 Esterel 프로그램으로부터 오토마타 생성이 필요하다. 생성된 오토마타는 다양한 오토마타 이론의 적용이 가능하고, 모델 체킹과 같은 다양한 분석에도 활용될 수 있다.
본 논문에서는 Esterel을 위한 Esterel 문법 구조 바탕의 오토마타 생성 규칙을 제안한다. 제안된 오토마타 생성 규칙은 다양한 분석에 유연하게 이용될 수 있다. 이 생성 규칙을 바탕으로 Esterel 프로그램으로부터 오토마타를 생성하기 위한 오토마타 생성 기반구조를 설계하였다. 우리의 생성 기반구조는 오토마타 생성과 더불어 이를 사용자가 생성된 오토마타를 이미지 형태로 관찰 할 수 있도록 출력한다. 특히 우리의 생성 기반구조는 사용자의 관심 대상을 입력으로 받아 이에 대한 오토마타만을 생성하도록 한다. 이는 전체 오토마타에서 사용자의 관심 대상 오토마타 상태만을 관찰할 수 있게 함으로써 오토마타의 활용도와 오토마타를 대상의 분석을 수행함에 있어서 효율성을 높이기 위함이다. 본 논문에서는 관심 대상을 출력 시그널에 초점을 맞추어 다루었다.
신호등 제어 시스템을 대상으로 오토마타 생성 기반구조에 대한 실험을 진행하였고, 실험을 통해서 전체 오토마타와 관심 대상 오토마타를 얻었다. 얻어진 실험 결과를 통해서 관심 대상 오토마타가 전체 오토마타에 비해서 많은 간선과 노드를 줄일 수 있음을 보일 수 있었다. 이를 통해서 우리가 제안하는 생성 규칙이 실제 분석에서 사용될 수 있음을 보였고, 또한 우리의 생성 기반 구조가 효과적으로 검증 및 테스팅 수행에 도움이 될 수 있음을 알 수 있었다.
