Timed verification with μCRL

Stefan Blom; Natalia Ioustinova; Natalia Sidorova

doi:10.1007/978-3-540-39866-0_20

Timed verification with μCRL

Stefan Blom, Natalia Ioustinova, Natalia Sidorova

Process Analytics

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

14 Citations (Scopus)

Abstract

μCRL is a process algebraic language for specification and verification of distributed systems. μCRL allows to describe temporal properties of distributed systems but it has no explicit reference to time. In this work we propose a manner of introducing discrete time without extending the language. The semantics of discrete time we use makes it possible to reduce the time progress problem to the diagnostics of "no action is enabled" situations. The synchronous nature of the language facilitates the task. We show some experimental verification results obtained on a timed communication protocol.

Original language	English
Title of host publication	Perspective of Systems Informatics (Proceedings 5th International Andrei Ershov Memorial Conference, PSI 2003, Akademgorodok, Novosibirsk, Russia. July 9-12, 2003)
Editors	M. Broy, A.V. Zamulin
Place of Publication	Berlin
Publisher	Springer
Pages	178-191
Number of pages	14
ISBN (Print)	3-540-20813-5
DOIs	https://doi.org/10.1007/978-3-540-39866-0_20
Publication status	Published - 2003

Publication series

Name	Lecture Notes in Computer Science
Volume	2890
ISSN (Print)	0302-9743

Keywords

μCRL
Discrete time
Model checking
Modelling
Verification

Access to Document

10.1007/978-3-540-39866-0_20

Cite this

Blom, S., Ioustinova, N., & Sidorova, N. (2003). Timed verification with μCRL. In M. Broy, & A. V. Zamulin (Eds.), Perspective of Systems Informatics (Proceedings 5th International Andrei Ershov Memorial Conference, PSI 2003, Akademgorodok, Novosibirsk, Russia. July 9-12, 2003) (pp. 178-191). (Lecture Notes in Computer Science; Vol. 2890). Springer. https://doi.org/10.1007/978-3-540-39866-0_20

@inproceedings{34e3fd6e46fd4679a47328cdca7ba815,

title = "Timed verification with μCRL",

abstract = "μCRL is a process algebraic language for specification and verification of distributed systems. μCRL allows to describe temporal properties of distributed systems but it has no explicit reference to time. In this work we propose a manner of introducing discrete time without extending the language. The semantics of discrete time we use makes it possible to reduce the time progress problem to the diagnostics of {"}no action is enabled{"} situations. The synchronous nature of the language facilitates the task. We show some experimental verification results obtained on a timed communication protocol.",

keywords = "μCRL, Discrete time, Model checking, Modelling, Verification",

author = "Stefan Blom and Natalia Ioustinova and Natalia Sidorova",

year = "2003",

doi = "10.1007/978-3-540-39866-0_20",

language = "English",

isbn = "3-540-20813-5",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "178--191",

editor = "M. Broy and A.V. Zamulin",

booktitle = "Perspective of Systems Informatics (Proceedings 5th International Andrei Ershov Memorial Conference, PSI 2003, Akademgorodok, Novosibirsk, Russia. July 9-12, 2003)",

}

Blom, S, Ioustinova, N & Sidorova, N 2003, Timed verification with μCRL. in M Broy & AV Zamulin (eds), Perspective of Systems Informatics (Proceedings 5th International Andrei Ershov Memorial Conference, PSI 2003, Akademgorodok, Novosibirsk, Russia. July 9-12, 2003). Lecture Notes in Computer Science, vol. 2890, Springer, Berlin, pp. 178-191. https://doi.org/10.1007/978-3-540-39866-0_20

Timed verification with μCRL. / Blom, Stefan; Ioustinova, Natalia; Sidorova, Natalia.
Perspective of Systems Informatics (Proceedings 5th International Andrei Ershov Memorial Conference, PSI 2003, Akademgorodok, Novosibirsk, Russia. July 9-12, 2003). ed. / M. Broy; A.V. Zamulin. Berlin: Springer, 2003. p. 178-191 (Lecture Notes in Computer Science; Vol. 2890).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Timed verification with μCRL

AU - Blom, Stefan

AU - Ioustinova, Natalia

AU - Sidorova, Natalia

PY - 2003

Y1 - 2003

N2 - μCRL is a process algebraic language for specification and verification of distributed systems. μCRL allows to describe temporal properties of distributed systems but it has no explicit reference to time. In this work we propose a manner of introducing discrete time without extending the language. The semantics of discrete time we use makes it possible to reduce the time progress problem to the diagnostics of "no action is enabled" situations. The synchronous nature of the language facilitates the task. We show some experimental verification results obtained on a timed communication protocol.

AB - μCRL is a process algebraic language for specification and verification of distributed systems. μCRL allows to describe temporal properties of distributed systems but it has no explicit reference to time. In this work we propose a manner of introducing discrete time without extending the language. The semantics of discrete time we use makes it possible to reduce the time progress problem to the diagnostics of "no action is enabled" situations. The synchronous nature of the language facilitates the task. We show some experimental verification results obtained on a timed communication protocol.

KW - μCRL

KW - Discrete time

KW - Model checking

KW - Modelling

KW - Verification

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

U2 - 10.1007/978-3-540-39866-0_20

DO - 10.1007/978-3-540-39866-0_20

M3 - Conference contribution

SN - 3-540-20813-5

T3 - Lecture Notes in Computer Science

SP - 178

EP - 191

BT - Perspective of Systems Informatics (Proceedings 5th International Andrei Ershov Memorial Conference, PSI 2003, Akademgorodok, Novosibirsk, Russia. July 9-12, 2003)

A2 - Broy, M.

A2 - Zamulin, A.V.

PB - Springer

CY - Berlin

ER -

Timed verification with μCRL

Abstract

Publication series

Keywords

Access to Document

Other files and links

Fingerprint

Cite this