Modeling scheduling policy with Constraint Satisfaction Problem approach

摘要

Many safety critical systems are real-time systems and a failure on the real-time property may cause serious damage on people and environment. Schedulability analysis is a good way of predicting system behavior and it is important for hard real-time tasks in which keeping deadline is critical. In this paper, we have proposed schedulability analysis with constraint solving approach. The behaviors of the scheduler are analyzed and decomposed into state-based behaviors in order to encode them into constraints. Then, constraints for task model are solved by SMT solver for satisfying interpretations. Treating schedulability analysis as a constraint satisfaction problem has some benefits. Constraints are focused on problems itself and it is based on logic formulas which are simple and clear. More importantly, modern SMT solvers can solve constraints in no time.