Abstract:
The pervasiveness, as well as the functionality and complexity of embedded systems have significantly increased in recent years. As a result, new challenges were brought to the designing tools. Synchronous programming languages are categorized as one class of the best available tools for designing embedded systems, providing support of concurrency and formal methods to verify embedded systems for safety critical applications. However, the determinism of concurrency relies upon the synchrony hypothesis, which must be verified through Worst Case Reaction Time (WCRT) analysis. The existing approaches for WCRT analysis are based on the techniques that are developed for Worst Case Execution Time (WCET) analysis, which may inefficient for WCRT analysis. This thesis addresses this issue and proposes a new Integer Linear Programming (ILP) based approach for WCRT analysis. The proposed approach is based on the synchronous programming language called Precision Timed C (PRET-C). The context in the synchronous program level is encoded in the WCRT analysis framework to improve the tightness of the WCRT estimations. For the purpose of evaluating the proposed approach, the state-of-the-art ILP based approach is replicated for PRET-C. The replicated approach is partially based on the existing techniques for WCET analysis. The two approaches are benchmarked in terms of WCRT tightness and analysis time. The obtained WCRT estimations are identical for both approaches. The analysis time of the replicated approach increases exponentially with the size and complexity of the benchmark programs. In comparison, the analysis time of the proposed approach does not show a clear trend of increase with the increase of size and complexity of the benchmark programs. The proposed approach is significantly faster than the replicated approach in large benchmark programs.