Asynchronous multi-process timed automata

Guoqiang Li, Li Liu, Akira Fukuda

Research output: Contribution to journalArticle

2 Citations (Scopus)

Abstract

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.

Original languageEnglish
Pages (from-to)961-989
Number of pages29
JournalSoftware Quality Journal
Volume26
Issue number3
DOIs
Publication statusPublished - Sep 1 2018

All Science Journal Classification (ASJC) codes

  • Software
  • Safety, Risk, Reliability and Quality

Fingerprint Dive into the research topics of 'Asynchronous multi-process timed automata'. Together they form a unique fingerprint.

  • Cite this