Projects per year
Abstract
This paper presents a new process algebra, called
PACoR, for realtime 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 densetime
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.
PACoR, for realtime 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 densetime
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.
Original language  English 

Number of pages  10 
Publication status  Published  2014 
Projects
 2 Finished

CRAFTERS: ConstRaint and Application driven Framework for Tailoring Embedded Realtime Systems
Skou, A., Larsen, K. G., Nielsen, B., David, A., Nyman, U., Mikucionis, M., Olsen, P., Boudjadar, J. & Kim, J. H.
01/06/2012 → 30/09/2015
Project: Research

MBAT: Modelbased Analysis and Testing of Embedded Systems
Nielsen, B., Larsen, K. G., David, A., Mikucionis, M. & Skou, A.
01/11/2011 → 31/10/2014
Project: Research