Model checking process algebra of communicating resources for real-time systems

Publication: ResearchWorking paper

Standard

Harvard

APA

CBE

MLA

Vancouver

Author

Bibtex

@techreport{ef74073a438142e498d36bf58a5bfa82,
title = "Model checking process algebra of communicating resources for real-time systems",
abstract = "This paper presents a new process algebra, calledPACoR, for real-time systems which deals with resource-constrained timed behavior as an improved version of theACSR algebra. We define PACoR as a Process Algebra ofCommunicating Resources which allows to explicitly expresspreemptiveness, urgentness and resource usage over a dense-timemodel. The semantic interpretation of PACoR is defined in theform of a timed transition system expressing the timed behaviorand dynamic creation of processes. We define a translation ofPACoR systems to Parameterized Stopwatch Automata (PSA).The translation preserves the original semantics of PACoR andenables the verification of PACoR systems using symbolic modelchecking in Uppaal and statistical model checking UppaalSMC.Finally we provide an example to illustrate system specificationin PACoR, translation and verification.",
author = "Jalil Boudjadar and Kim, {Jin Hyun} and Larsen, {Kim Guldstrand} and Ulrik Nyman",
year = "2014",
type = "WorkingPaper",

}

RIS

TY - UNPB

T1 - Model checking process algebra of communicating resources for real-time systems

AU - Boudjadar,Jalil

AU - Kim,Jin Hyun

AU - Larsen,Kim Guldstrand

AU - Nyman,Ulrik

PY - 2014

Y1 - 2014

N2 - This paper presents a new process algebra, calledPACoR, for real-time systems which deals with resource-constrained timed behavior as an improved version of theACSR algebra. We define PACoR as a Process Algebra ofCommunicating Resources which allows to explicitly expresspreemptiveness, urgentness and resource usage over a dense-timemodel. The semantic interpretation of PACoR is defined in theform of a timed transition system expressing the timed behaviorand dynamic creation of processes. We define a translation ofPACoR systems to Parameterized Stopwatch Automata (PSA).The translation preserves the original semantics of PACoR andenables the verification of PACoR systems using symbolic modelchecking in Uppaal and statistical model checking UppaalSMC.Finally we provide an example to illustrate system specificationin PACoR, translation and verification.

AB - This paper presents a new process algebra, calledPACoR, for real-time systems which deals with resource-constrained timed behavior as an improved version of theACSR algebra. We define PACoR as a Process Algebra ofCommunicating Resources which allows to explicitly expresspreemptiveness, urgentness and resource usage over a dense-timemodel. The semantic interpretation of PACoR is defined in theform of a timed transition system expressing the timed behaviorand dynamic creation of processes. We define a translation ofPACoR systems to Parameterized Stopwatch Automata (PSA).The translation preserves the original semantics of PACoR andenables the verification of PACoR systems using symbolic modelchecking in Uppaal and statistical model checking UppaalSMC.Finally we provide an example to illustrate system specificationin PACoR, translation and verification.

M3 - Working paper

BT - Model checking process algebra of communicating resources for real-time systems

ER -

ID: 195304511