High-Level Execution Time Analysis

Farn Wang

psfileTR-IIS-97-009


Keywords:
real-time, specification, verification, software recursion, context-free, semilinear

Abstract

A compositional algebra, called mMCAN, for the execution time analysis of high-level software processes is introduced. In mMCAN, processes can be concatenated, concurrently executed, and recursively invoked. We show that the set of execution times of an mMCAN is semilinear. We then propose and analyze an algorithm which calcuates the execution time sets of an mMCAN in semilinear forms. Finally, we consider several interesting variations of mMCAN whose execution time sets can be computed with algorithms.