Timing analysis is an essential process for development of real-time embedded system and knowledge about the worst-case execution time (WCET) is crucial to validation of temporal correctness of implemented system. Research on automated static timing analysis is actively in progress to complement limitation of traditional timing measurement method. Automated static timing analysis methods provide safe but usually overestimated worst-cast execution time (WCET). Overestimation is mainly due to the existence of execution paths which turn out to be infeasible or impractical if dynamic behaviors of a program or environmental assumptions are fully considered. Therefore, user annotation of additional flow information is required for static WCET analyzer to get a tighter WCET estimation.
In this thesis, we propose a new method and a visual language, User Constraint Language (UCL), to facilitate the specification of user constraints. In our method, both program and flow information are represented by single formalism-finite automata. UCL provides intuitive visual notations with which users can easily specify various levels of flow information to characterize execution paths of program. User constraints specified in UCL formulas are converted into corresponding finite automata. They are combined with the automaton representing the control flow graph of a target program through cross production. The combined automaton reflects the static structure and possible dynamic behavior of the program, and does not contain infeasible or impractical execution paths that are the main cause of loose estimation of WCET.
We describe the visual notation and textual formula of UCL with examples which illustrate their usage. Then we define the formal syntax and semantics of UCL and propose a translation scheme to convert UCL formulas into finite automata. We also present a method to check the consistency of user-provided UCL constraints. UCL can specify complex flow information to eliminate infeasible or impractical paths that are difficult or impossible to specify in other flow representation languages. It is also neutral to the back-end calculation methods so it can be applied to the path-based or IPET-based static WCET calculation method. A case study using part of a software program for satellite flight demonstrates the effectiveness of UCL and our approach.
실시간 시스템 소프트웨어는 정해진 시간 내에 필요한 작업을 수행하여야 하므로 각 소프트웨어 수행 타이밍 분석이 필수적이며 이 중 최장수행시간을 구하는 것이 중요하다. 기존의 실시간 시스템 소프트웨어의 타이밍 분석은 개발자의 수작업에 의존하여 많은 시간과 노력이 요구되며 정확성에 문제가 있을 수 있는 단점이 있었다. 이를 해결하기 위해 자동화된 정적 타이밍 분석에 대한 연구가 활발히 진행되고 있다. 자동화된 정적 타이밍 분석기법은 실제로 목적시스템에서 소프트웨어를 수행하여 타이밍을 측정하는 대신 프로그램 코드와 대상 하드웨어 시스템 특성을 분석함으로써 최장수행시간을 예측하는 기법이다. 그러나 정적 타이밍 분석기법은 실제 프로그램의 동적 행위나 프로그램이 수행되는 환경에 대한 가정이 충분히 고려되지 않을 경우 실제보다 과대평가된 최장수행시간을 제공한다. 보다 정확히 최장수행시간을 예측하기 위해서는 사용자가 추가로 프로그램 제어흐름에 대한 정보를 제공하여야 한다.
본 논문에서는 사용자 제약사항의 명세를 위한 새로운 방법과 시각적 언어인 UCL (User Constraint Language)를 제안한다. 본 논문은 소프트웨어 프로그램과 제어흐름 정보를 finite automata로 정형화하여 나타낸다. UCL언어는 직관적인 시각적 기호를 제공하여 사용자가 프로그램 수행경로를 제한하기 위한 다양한 수준의 제어흐름 정보를 기술 가능하게 한다. 사용자가 UCL로 기술한 제약사항은 finite automata로 변환되며, 프로그램의 제어흐름도를 나타내는 finite automaton과 결합된다. 결합된 finite automaton은 사용자가 제한한 프로그램 수행경로만을 포함하고 있어 이로부터 path-based 또는 IPET-based 계산기법을 사용하여 보다 정확한 최장수행시간 예측 치를 구할 수 있게 된다. 본 논문에서는 UCL 언어의 시각적 기호의 사용법을 예를 들어 기술하고 UCL의 formal syntax 및 semantics를 정의하였다. 또 UCL 공식을 finite automata로 변환하고 이들 간의 consistency를 검사하는 알고리즘을 제시하였다. 이를 기존의 정적 타이밍 분석도구에 구현하고 인공위성 소프트웨어에 적용하여 기존의 언어로는 명세하기 어려운 프로그램 제어흐름 정보를 UCL을 사용하여 기술함으로써 보다 정확한 최장수행시간을 구할 수 있음을 실증하였다. 또한 본 논문에서 제시한 UCL은 특정한 계산기법에 제한되지 않고 path-based 나 IPET-based 기법에 모두 적용 가능한 장점이 있다.
