Time-Sensitive Pushdown Systems

With the wide use of large scale and complex real-time embedded system,the real-time requirement of program execution receives more and more attention.Time-Sensitive pushdown systems are a kind of systems with timed constraints during context switch.It shows both the theoretical and practical importance in program analysis and system verification with time requirements.At present,the research for the verification of time-sensitive context switching system is not mature enough,and the related results are few,so it is worthy of attention and research.In the time-sensitive pushdown systems,clocks used to constrain the behaviours of realtime systems can be divided into global clocks(all contexts can modify their values and subject to their constraints),local clocks(only the current context can modify their value and subject to their constraints),frozen clocks(these clocks bind themself with the current context.If the context switches,these clocks will stop running until the current context is returned)and updatable clock(these clocks are allowed to increment and decrement by one).The timed constraints used to test can be divided into diagonal-free constraints(allow to test whether the value of clock is in some interval)and diagonal constriants(further allow to test whether the difference of values of two clocks is in some interval).In the field of real-time verification,the problem of system verification under different kinds of clocks and different kinds of timed constraints is a hot research issue.The main contribution of this thesis are the results about the following three issues of timesensitive pushdown systems,based on one kind of time sensitive pushdown system,nested timed automata: Firstly,for the reachability problem of the generalized nested timed automata,it is proved to be undecidable,and it is decidable when the frozen clock is not allowed;Secondly,for the problem of state reachability for nested timed automata under diagonal-free constraints,a forward over-approximation algorithm is presented and a proof of its correctness is given;Thirdly,for the reachability problem of updatable timed automata with one updatable clock,it is proved to be undecidable under diagonal constraints and decidable under diagonal-free constraints.Although these results are based nested timed automata,it is easy to extend to other time-sensitve pushdown systems.The decidability results for time-sensitive pushdown systems in this thesis can fill the gaps in the current research,and pave the way for the efficient tools of time sensitive pushdown systems.