High-quality asynchronous programs are needed urgently to exploit multi-core hardware and cloud platforms. However, in real-time systems, formal models such as timed automata (TAs) are limited to concurrent programs where the number of processes is constant and no process is triggered on-the-fly. To better support the verification of asynchronous programs, we propose a new model called asynchronous multi-process timed automata (APTAs) based on TAs. Processes are abstracted as process timed automata (PTAs), which are almost the same as TAs except some states are for triggering new processes. A multiset is used to buffer triggered instances. The model is sufficiently expressive to describe real-time asynchronous programs with dynamic process creation. We show that the coverability problem, which is used for checking safety property of programs, is decidable by encoding it into read-arc timed Petri nets (RTPNs). We then propose an algorithm for the coverability problem and provide a proof of the termination and correctness.
All Science Journal Classification (ASJC) codes
- Safety, Risk, Reliability and Quality