Handling overloads in dynamic real-time embedded systems which are subject to frequent workload changes is a critical issue as it allows graceful quality of service (QoS) degradation and provides a mechanism to determine the load to be shed to handle the overload. This paper presents a novel hybrid automata based ERfair scheduling framework for a real-time system which may be subjected to transient overloads. Each task has an assigned criticality value and consists of two parts, a mandatory part and an optional part. The probability distribution of task arrivals is assumed to be known in advance. The framework employs a formal automata based a priori analysis mechanism for detecting and avoiding possible overload within a stipulated time in future. The proposed formal model is verifiable, thereby making it suitable to model a complex system. The verifiable model ensures that all possible cases of overloads are detected and chances of false positives are minimized, thereby maximizing resource utilization.