Migration of Legacy Software Towards Correct-by-Construction Timing Behavior

Date Added: Sep 2010
Format: PDF

This paper presents an approach for incrementally adjusting the timing behavior of legacy real-time software according to explicit timing specifications expressed in the Timing Definition Language (TDL). The primary goal of such a migration is to achieve predictable timing behavior, which enables application of formal verification methods to the legacy system. The approach entails a minimal instrumentation of the original code combined with an automatically generated runtime system, which ensures that the executions of designated periodic computations in the legacy software satisfy the logical execution time specifications of the TDL model.