The Coverability Problem Of Asynchronous Multi-Process Timed Automata

In recent years,high quality asynchronous programs are needed urgently to benefit from multi-core hardwares and cloud platforms.However in real-time systems,asynchronous programs still suffer from a lack of analysis and verification tools.Formal models like Timed automata are limited to concurrent programs where the number of processes is constant and no process is triggered on the fly.To support the verification of asynchronous programs well,this paper proposes a new model named asynchronous multi-process timed automata: processes are abstracted as process timed automata which are almost the same with timed automata except some states are for triggering new processes;a multiset is used to buffer triggered instances;processes trigger other processes without being blocked and run asynchronously with triggered processes.The asynchronous multi-process timed automata is powerful enough to model many complex real-time asynchronous programs.The safety properties of real-time asynchronous programs can be verified by the algorithm of the coverability problem.In this paper,we concentrate on the research of the formal semantics,the decidability of the coverability problem and the algorithm of the coverability problem of asynchronous multi-process timed automata:· This paper defines the semantics of asynchronous multi-process timed automata as follows:progress transition for evolving the system synchronously with time;activation transition for running the process instance in the buffer set;action transition for a inner statement in a process instance;triggering transition for generating new process instance in the buffer set;finishing transition for finishing a process instance.The semantics are powerful enough to model many useful real-time asynchronous programs while preserving the decidability of the coverability problem.Also they make it relative easy to describe complex real-time asynchronous programs while retaining themselves simple.· Many safety properties of a system can be reduced to the coverability problem.The research of the decidability of the coverability problem,on the one hand,ensures that thesafety properties of the model can be verified;on the other hand,enables the adjustment of the semantics when the coverability problem is not decidable.It's difficult to proof the decidability of the coverability problem directly,we proof it by encoding the model to read-arc timed petri nets.We impose restriction on the semantics to make the encoding possible.· It's difficult to design the algorithm of the coverability problem since there are infinite system configurations.We use a data structure named existential zones,a extension of zones used in the algorithm of the reachability problem of the timed automata.By repeatedly computing the Pre set of the existential zones,the algorithm reaches a fix-point set Z.The coverability problem is then reduced to whether the initial configuration is in all configurations represented by all existential zones in Z.