Model Checking Process Algebra of Communicating Resources for Real-time Systems

Publikation: Forskning - peer reviewKonferenceartikel i proceeding

Standard

Model Checking Process Algebra of Communicating Resources for Real-time Systems. / Boudjadar, Jalil; Kim, Jin Hyun; Larsen, Kim Guldstrand; Nyman, Ulrik.

Proceedings of ECRTS 2014. IEEE Press, 2014. s. 51-60 (Euromicro Conference on Real-Time Systems. Proceedings).

Publikation: Forskning - peer reviewKonferenceartikel i proceeding

Harvard

Boudjadar, J, Kim, JH, Larsen, KG & Nyman, U 2014, Model Checking Process Algebra of Communicating Resources for Real-time Systems. i Proceedings of ECRTS 2014. IEEE Press, s. 51-60. Euromicro Conference on Real-Time Systems. Proceedings, DOI: 10.1109/ECRTS.2014.24

APA

Boudjadar, J., Kim, J. H., Larsen, K. G., & Nyman, U. (2014). Model Checking Process Algebra of Communicating Resources for Real-time Systems. I Proceedings of ECRTS 2014 (s. 51-60). IEEE Press. (Euromicro Conference on Real-Time Systems. Proceedings). DOI: 10.1109/ECRTS.2014.24

CBE

Boudjadar J, Kim JH, Larsen KG, Nyman U. 2014. Model Checking Process Algebra of Communicating Resources for Real-time Systems. I Proceedings of ECRTS 2014. IEEE Press. s. 51-60. (Euromicro Conference on Real-Time Systems. Proceedings). Tilgængelig fra: 10.1109/ECRTS.2014.24

MLA

Boudjadar, Jalil et al. "Model Checking Process Algebra of Communicating Resources for Real-time Systems". Proceedings of ECRTS 2014. IEEE Press. 2014. 51-60. (Euromicro Conference on Real-Time Systems. Proceedings). Tilgængelig: 10.1109/ECRTS.2014.24

Vancouver

Boudjadar J, Kim JH, Larsen KG, Nyman U. Model Checking Process Algebra of Communicating Resources for Real-time Systems. I Proceedings of ECRTS 2014. IEEE Press. 2014. s. 51-60. (Euromicro Conference on Real-Time Systems. Proceedings). Tilgængelig fra, DOI: 10.1109/ECRTS.2014.24

Author

Boudjadar, Jalil; Kim, Jin Hyun; Larsen, Kim Guldstrand; Nyman, Ulrik / Model Checking Process Algebra of Communicating Resources for Real-time Systems.

Proceedings of ECRTS 2014. IEEE Press, 2014. s. 51-60 (Euromicro Conference on Real-Time Systems. Proceedings).

Publikation: Forskning - peer reviewKonferenceartikel i proceeding

Bibtex

@inbook{16b13dde563e4a5597c0b07fb53b1fc2,
title = "Model Checking Process Algebra of Communicating Resources for Real-time Systems",
abstract = "This paper presents a new process algebra, called 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 express preemptiveness, urgent ness 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 UPPAAL SMC. Finally we provide an example to illustrate system specification in PACOR, translation and verification.",
author = "Jalil Boudjadar and Kim, {Jin Hyun} and Larsen, {Kim Guldstrand} and Ulrik Nyman",
year = "2014",
doi = "10.1109/ECRTS.2014.24",
isbn = "978-1-4799-5797-2",
pages = "51--60",
booktitle = "Proceedings of ECRTS 2014",
publisher = "IEEE Press",

}

RIS

TY - GEN

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, called 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 express preemptiveness, urgent ness 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 UPPAAL SMC. Finally we provide an example to illustrate system specification in PACOR, translation and verification.

AB - This paper presents a new process algebra, called 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 express preemptiveness, urgent ness 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 UPPAAL SMC. Finally we provide an example to illustrate system specification in PACOR, translation and verification.

U2 - 10.1109/ECRTS.2014.24

DO - 10.1109/ECRTS.2014.24

M3 - Article in proceeding

SN - 978-1-4799-5797-2

SP - 51

EP - 60

BT - Proceedings of ECRTS 2014

PB - IEEE Press

ER -

ID: 209589451