On inspection and verification of software with timing requirements

摘要

Software with hard timing requirements should be designed using a systematic approach to make its timing properties easier to inspect and verify; otherwise, it may be practically impossible to determine whether the software satisfies the timing requirements. Pre-runtime scheduling provides such an approach by placing restrictions on software structures to reduce complexity. A major benefit of using a pre-runtime scheduling approach is that it makes it easier to systematically inspect and verify the timing properties of the actual software code, not just various high-level abstractions of the code.