Many embedded systems are safety-critical, and their defects become more critical to our lives because they are pervasive in the modern life. The testing of safety-critical applications must be done thoroughly with high accuracy, which makes the process costly and acute. Most embedded systems are categorized into control-dominated reactive applications.
To improve the reliability of reactive systems, a variety of formal verification and testing tools have been developed, but debuggers are usually one of the most useful tools for developers to find casual errors in reactive programs. Testing and verification methods are often applied after programs have been developed. To verify the correctness of programs, writing precise properties is a hard task because these properties have to be tested, or proved, or debugged recursively. Moreover, programmers sometimes want simple validations that can be applied while the system is under development.
In this thesis, we select Esterel as our target language for programming synchronous reactive embedded systems. Then, we suggest the scheme to generate test input sequences automatically to verify properties for programmers to prove. We propose the debugger for Esterel that has the following features: (i) accessibility which means that any Esterel program can be debugged when the complete source codes of a module and its components are available and (ii) easy usage which means that user can describe properties with very simple specifications. We adopt the test case generation process as a debugging method that generates input signal sequences that drive a program to reach a targeted state. We demonstrate that our methodology of debugger is useful with a case study in which our method analyzes the railroad crossing system for railroad management and generates test cases to prove the properties of interests.
오늘날 임베디드 시스템은 항공, 우주, 의료 등을 포함하는 안전성 중점 시스템 (safety-critical system)에서 널리 사용되고 있으며, 따라서 임베디드 시스템의 오류가 사회에 미치는 파급 효과를 고려해 봤을 때 임베디드 시스템의 신뢰성을 확보하는 일은 그것의 개발에 있어 매우 중요한 과정이다. 그리고 시스템 개발을 위한 전체 과정 중 신뢰성 확보에 가장 큰 역할을 담당하는 검증 과정 (verification process)은 결과 시스템의 신뢰도뿐만 아니라 개발에 소요되는 전체 비용에도 매우 큰 영향을 준다. 대부분의 임베디드 시스템은 제어에 의해 운용되는 상호 작용 시스템으로 분류된다.
상호 작용 시스템의 신뢰도 향상을 위해 다양한 정형 검증과 테스트 케이스 생성에 대한 기법들이 연구되어 왔지만, 이 방법들은 프로그램의 개발이 완료된 후에야 적용 가능한 경우가 대부분이다. 또한 검증을 위해 속성을 기술하는 어려운 작업이 수반되며 이때 기술된 속성 자체도 검증되어야 한다. 따라서 정형 검증 방법의 한계를 보완하여 전체 시스템에 대한 완성도 높은 검증을 하기 위해 여전히 프로그램을 디버깅하는 방법에 대한 연구가 진행되고 있다.
이 논문에서는 동기화된 상호 작용 프로그램의 구현을 위해 Esterel이라는 언어를 사용한다. 그리고 Esterel 프로그램의 검증을 위해 사용되는 정형 검증 방법들을 보완하기 위한 디버깅 도구를 제안한다. 이 논문이 제안하고 있는 디버깅 도구는 1. 접근의 용이성과 2. 사용에 있어서의 편리함을 장점으로 한다. 접근의 용이성이라 함은 Esterel 프로그램 개발의 어느 단계에서의 어느 모듈에 대해서라도 Esterel의 기본적인 문법 조건을 갖춘 소스 코드에 대한 디버깅이 가능해야 함을 의미한다. 또한 사용에 있어서의 편리함은 확인하고자 하는 속성, 또는 소스 코드의 특정 실행 상태를 정의함에 있어 그 표현 방식의 작성 규칙이나 이해가 어렵지 않아야 함을 의미한다. Esterel 프로그램의 디버깅 방법으로 정의된 속성에 대한 테스트 데이터 생성이라는 방법을 채택하였고 이 때 생성되는 테스트 데이터인 일련의 입력 신호 집합의 흐름은 프로그램을 디버깅 하고자 하는 속성을 의미하는 특정 상태로 도달하도록 유도하는 자료가 된다.
마지막으로 제안하고 있는 디버깅 도구의 실효성을 보이기 위해 철도 건널목 예제를 제시하고 특정 속성에 대한 테스트 데이터 생성 결과를 보인다.
