Schedulability Analysis Of Timed Regular Tasks Automata

Real-timed systems play a crucial role in critical applications such as defense,finance,telecommunication and so on.In recent years,a large number of real-time systems used in our daily and industrial production.Real-timed systems not only should guarantee the logical correctness,but also the correctness of time.Schedulability analysis is a method used to check whether all tasks in a real-timed system can finish within their relative deadline under a scheduling strategy.Therefore,schedulability analysis is a core problem in development and analysis of real-time systems.In the area of formal verification,timed automata(TAs)are usually used to model real-timed systems.In the late 1990 s,Elena Fersman et al.proposed task automata which extended timed automata to do scheduling analysis.Given a task system,each task is usually characterized by a worst-case execution time(WCET),a best-case execution time(BCET)and a relative deadline.Getting the worst-case execution time is a prerequisite for many schedulability analysis methods.However,in reality,a task is usually too complex to calculate the WCET,even the task is abstracted to a formal model.WCET is a pessimistic estimate which will never reach in a actual situation.In this paper,we propose a model named timed regular task automata(TRTAs)extended task automata to model real-timed system.A timed regular task automaton is essentially a timed automaton,so it can control the behavior of task arrival.In a timed regular task automaton,a control location can be assigned a task.Each task is characterized by a timed automaton,a starting point with initial clock valuation,a status and a relative deadline,where the timed automaton is used to describe the behavior of the task,and the status of the task can be released,running,preempted and so no,so this model supports preemptive scheduling strategies.Timed regular task automata have powerful expression so that it can model many complex real-timed systems.Based on timed regular task automata,this paper proposes a scheduling method without the information of WCET.A test is performed on each timed automaton to get an underapproximation of the WCET.What is more,there is an obvious observation that a schedulable task queue is bounded,the boundary can calculate with the relative deadline and execution time of tasks.If the length of a task queue exceeds the boundary,the system is non-schedulable,otherwise,a further schedulability checking is performed.We encode the schedulability analysis problem into the reachability problem of nested timed automata which is proved decidable,so that we can prove our method is decidable.