Nested Timed Automata,Revisited

Currently more and more real-time systems are used in our daily life,such as software systems in trafic lights,elevators and aircrafts.Misbehaviors of these systems could lead to huge economic losses of society,so verification of correctness of such systems is important.Generating lots of test cases and checking behaviours is a good way,but since the test cases are finite,there are always test cases which cannot be covered.Thus verifying by test cases is not a complete method intrinsicaly.Formal methods,or more specifically,model checking,is a sound and complete method for verification of hardware and software systems.Given a model of a system,it checks whether the model satisfies some properties,like safety properties and liveness properties.Unfortunately,some properties in some models are undecidable.For example,in Turing machines,which are powerful and can execute any program that a computer can,the halting problem is undecidable.So researchers would like to find suitable and decidable models for their target systems.Timed automata is a popular model for verifications of real-time systems.Many properties on it are decidable,so lots of tools based on it are proposed,such as UPPAL.However,it cannot be directly applied to real-times systems with recursions.More powerful models are needed to verify such systems.To address this problem,nested timed automata((NeTA)is proposed and researched.NeTA is a pushdown system where each stack frame contains a timed automaton.A timed automaton can be suspended and pushed to the stack,or poped back from the stack and resume running.These push and pop operations are perfectly for modeling recursions in programs.A lot of properties and extensions of NeTA have already been researched,such as frozen clocks,diagonal constraints,algorithms on reachability and schedulability.This thesis continues this research and has the following contributions.This thesis introduces a model named nested updatable timed automata(NeUTA),which can be regarded as a combination of nested timed automata and updatable timed automata with one updatable clock(UTA1).The model is suitable for soft real-time system analysis,since the updatable clock representing a deadline can be updated due to environments.This thesis shows the termination and boundedness of NeUTA are decidable.This thesis introduces a model named nested timed automata with invariants(NeTA-I),which extends NeTA with invariants.Invariants are usually adopted into timed systems to constrain the time passage within each control location.It is well-known that a timed automaton with invariants can be encoded to an equivalent one without invariants.When recursions are taken into consideration,few results show whether invariants affect expressiveness.This thesis investigates the effect of invariants to NeTA.In particular,this thesis studies the reachability problem for NeTA-I.It is shown that the reachability problem is undecidable on NeTA-I with a single global clock,while it is decidable when no invariants are given.Furthermore,this thesis also shows that the reachability is decidable if the NeTA-I contains no global clocks by showing that a good stack content still satisfies well-formed constraints.