Task Modeling And Scheduling Analysis In Uniprocessor Environment Based On CCSL

Clock Constraint Specification Language(CCSL)is a modeling language based on logic clock that can be used to describe the temporal behavior of real-time embedded systems.The advantage of CCSL is that it can describe the time requirements of tasks without reference to physical clocks,and can express the interaction requirements between modules with the help of the constraint relationship between logic clocks.Through the formal analysis of CCSL,not only the scheduling analysis of CCSL constraints can be carried out,but also relevant theoretical proof can be further carried out,or the properties of complex systems can be verified by model checking.Modeling and analysis based on a certain scheduling policy is a classic problem in traditional real-time task scheduling,especially in a uniprocessor environment.However,current CCSL-based real-time task scheduling analysis does not support scheduling policy modeling and analysis.It is beneficial to expand the modeling ability and application scope of CCSL to realize real-time task scheduling under specific policies based on CCSL.Taking uniprocessor task scheduling as an example,this paper proposes a scheduling policy-oriented CCSL scheduling analysis method.By combining priority-driven and other policy ideas,the work abstracts the characteristic events of a scheduling policy as logic clocks and add CCSL constraints between logic clocks to obtain a constraint set.After the CCSL constraint set is transformed into SMT formulas,the SMT solver then solves the SMT formulas and finally obtains the unique optimal scheduling solution.With the method,real-time scheduling policy modeling of CCSL in uniprocessor environment is implemented,and CCSL semantic set is extended in the process of scheduling policy transformation into CCSL constraints.Ultimately,this paper integrates two functional modules——the task model conversion to CCSL constraints module and the CCSL constraints solver module,into the tool 'Task2CCSL'.The effectiveness of the proposed method is demonstrated by solving simplified real-time scheduling problems in a uniprocessor environment.