The application considered is mixed-criticality scheduling. The core formal approaches used are Rely-Guarantee conditions and the Timeband framework; these are applied to give a layered description of job scheduling which includes resilience to jobs overrunning their expected execution time. A novel formal modelling idea is proposed to handle the relationship between actual time and its approximation in hardware clocks.

翻译：所考虑的应用程序是混合临界时间表,采用的核心正式办法为Rely-Guarantee条件和时间带框架;这些办法用于对工作时间安排进行分层描述,其中包括对超过预期执行时间的工作的复原力,提出了一个新的正式模型构想,以处理实际时间与硬件时钟近似之间的关系。