Replacing conjectures by positive knowledge: Inferring proven precise worst-case execution time bounds using symbolic execution

摘要

Embedded real-time software systems (ESS) play an important role in almost every aspect of our daily lives. We do rely on them to be functionally correct and to adhere to timing-constraints ensuring that their computational results are always delivered in time. Violations of the timing-constraints of a safety-critical ESS, such as an airplane or a medical control device, can have disastrous economic and social consequences. Identifying and correcting such violations is therefore an important and challenging research topic.