Resumé
PACoR, for real-time systems which deals with resource-
constrained timed behavior as an improved version of the
ACSR algebra. We define PACoR as a Process Algebra of
Communicating Resources which allows to explicitly express
preemptiveness, urgentness and resource usage over a dense-time
model. The semantic interpretation of PACoR is defined in the
form of a timed transition system expressing the timed behavior
and dynamic creation of processes. We define a translation of
PACoR systems to Parameterized Stopwatch Automata (PSA).
The translation preserves the original semantics of PACoR and
enables the verification of PACoR systems using symbolic model
checking in Uppaal and statistical model checking UppaalSMC.
Finally we provide an example to illustrate system specification
in PACoR, translation and verification.
| Originalsprog | Engelsk |
|---|---|
| Antal sider | 10 |
| Status | Udgivet - 2014 |
Citer dette
}
Model checking process algebra of communicating resources for real-time systems. / Boudjadar, Jalil; Kim, Jin Hyun; Larsen, Kim Guldstrand; Nyman, Ulrik.
2014.Publikation: Working paper › Forskning
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 -