The Extension And Optimization Of Controller Synthsis Tool CTAV-TGA

Real-time systems are becoming pervasive.Typical examples of real-time systems include Air Traffic Control Systems,Networked Multimedia Systems,Command Control Systems etc.In a real-time System the correctness of the system behavior depends not only on the logical results of the computations,but also on the physical instant at which these results are produced.A missed deadline in hard real-time systems is catastrophic and in soft real-time systems it can lead to a significant loss.Hence it is important to ensure the reliability of real-time systems.Model checking is a popular technique for automatically verifying correctness properties of finite-state systems.Since 1990s,model checking has been applied to ensure the reliability of real-time systems.The real-time systems in model checking are closed,they will not be affected by external environment.But real-time systems are usually open in reality.The open real-time system can respond to external event caused by environment.An ideal solution would be to compute(we say synthesize in the sequel)a controller(if there is one)such that the correctness property is satisfied.This is the controller synthesis problem for open real-time systems.Before building a controller we still have to check if one exists,and this is the control problem formally defind by:given S and is there any C such that C(S)|=Φ?where S is a model the system to be controlled,C is a controller and Φ is the correctness property.CTAV-TGA is developed for controller synthsis problem based on model checking tool CTAV.We have implemented algorithms for solving timed games based on four types of winning conditions:<>p,[]p,[]<>p,<>[]p where p is a atomic proposition.But there are some deficiencies in sematic integrity and efficiency of CTAV-TGA.In this peper,we improve the CTAV-TGA based on sematics of invariant and uncontrollable actions.The deadlock states are considered,we back-propagate losing information of deadlock states,our algorithm terminates earlier with this optimization.In order to get a greater efficiency,we optimize algorithms with multi-core technique.