Towards a Generic Framework for Formal Verification and Performance Analysis of Real-Time Scheduling Algorithms

摘要

In real-time systems, several tasks must be executed under strict time constraints. The time requirements satisfaction depends considerably on task scheduling algorithms. Thus, performance analysis, formal verification, and comparison between a set of existing scheduling algorithms or newly proposed ones in such systems could be of great interest to designers. However, when systems are complex, models are typically used to represent their various aspects and evaluate their performance. In this paper, we propose a generic scalable framework for the description, analysis, and verification of various types of scheduling protocols based on periodic task models with the integration of their task splitting versions. The proposed framework is hierarchical based on a graphical formal model defined as a network of timed automata. This model is generic as it can be easily instantiated to describe widely used scheduling protocols or any newly proposed ones. Such modeled protocols are then formally analyzed and a set of their crucial properties is formally verified. We evaluate the feasibility of the proposed approach by implementing well-known load-balancing heuristic-based protocols.