Asynchronous multi-process timed automata

Guoqiang Li, Li Liu, Akira Fukuda

Research output: Contribution to journalArticle

1 Citation (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

Fingerprint

Real time systems
Petri nets
Computer hardware

All Science Journal Classification (ASJC) codes

  • Software
  • Safety, Risk, Reliability and Quality

Cite this

Asynchronous multi-process timed automata. / Li, Guoqiang; Liu, Li; Fukuda, Akira.

In: Software Quality Journal, Vol. 26, No. 3, 01.09.2018, p. 961-989.

Research output: Contribution to journalArticle

Li, Guoqiang ; Liu, Li ; Fukuda, Akira. / Asynchronous multi-process timed automata. In: Software Quality Journal. 2018 ; Vol. 26, No. 3. pp. 961-989.
@article{9996436b9d074af8af8e9efa8ea38071,
title = "Asynchronous multi-process timed automata",
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.",
author = "Guoqiang Li and Li Liu and Akira Fukuda",
year = "2018",
month = "9",
day = "1",
doi = "10.1007/s11219-017-9380-8",
language = "English",
volume = "26",
pages = "961--989",
journal = "Software Quality Journal",
issn = "0963-9314",
publisher = "Springer New York",
number = "3",

}

TY - JOUR

T1 - Asynchronous multi-process timed automata

AU - Li, Guoqiang

AU - Liu, Li

AU - Fukuda, Akira

PY - 2018/9/1

Y1 - 2018/9/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=85025064512&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85025064512&partnerID=8YFLogxK

U2 - 10.1007/s11219-017-9380-8

DO - 10.1007/s11219-017-9380-8

M3 - Article

AN - SCOPUS:85025064512

VL - 26

SP - 961

EP - 989

JO - Software Quality Journal

JF - Software Quality Journal

SN - 0963-9314

IS - 3

ER -