Integrating Formal Timing Analysis in the Real-Time Software Development Process

When designing complex real-time software, it is very difficult to predict how design decisions may impact the system timing behavior. Usually, the industrial practices rely on the subjective judgment of experienced software architects and developers. This is however risky since eventual timing errors are only detected after implementation and integration, when the software execution can be tested on system level, under realistic conditions. At this stage, timing errors may be very costly and time consuming to correct. Therefore, to overcome this problem we need an efficient, reliable and automated timing estimation method applicable already at early design stages and continuing throughout the whole development cycle. Formal timing analysis appears at first sight to be the adequate candidate for this purpose. However, its use in the industry is conditioned by a smooth and seamless integration in the software development process. This is not an easy task due to the semantic mismatches between the design and analysis models but also due to the missing link between the analysis and the testing phase after code implementation. In this paper, we present a timing analysis framework we developed in the context of the industrial design of satellite on-board software, allowing an early integration and full automation of formal timing verification activities in the development process of real-time embedded software, as a mean to decrease the design time and reduce the risks of costly timing failures.