An Abstraction Technique for Describing Concurrent Program Behaviour

Wytse Oortwijn, Stefan Blom, Dilian Gurov, Marieke Huisman, M. Zaharieva

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

This paper presents a technique to reason about functional properties of shared-memory concurrent software by means of abstraction. The abstract behaviour of the program is described using process algebras. In the program we indicate which concrete atomic steps correspond to the actions that are used in the process algebra term. Each action comes with a specification that describes its effect on the shared state. Program logics are used to show that the concrete program steps adhere to this specification. Separately, we also use program logics to prove that the program behaves as described by the process algebra term. Finally, via process algebraic reasoning we derive properties that hold for the program from its abstraction. This technique allows reasoning about the behaviour of highly concurrent, non-deterministic and possibly non-terminating programs. The paper discusses various verification examples to illustrate our approach. The verification technique is implemented as part of the VerCors toolset. We demonstrate that our technique is capable of verifying data- and control-flow properties that are hard to verify with alternative approaches, especially with mechanised tool support.
LanguageEnglish
Title of host publicationVerified Software. Theories, Tools, and Experiments
Subtitle of host publication9th International Conference, VSTTE 2017, Heidelberg, Germany, July 22-23, 2017, Revised Selected Papers
EditorsAndrei Paskevich, Thomas Wies
PublisherSpringer
Pages191-209
Number of pages19
ISBN (Electronic)978-3-319-72308-2
ISBN (Print)978-3-319-72307-5
DOIs
StatePublished - 2017
Event9th Working Conference on Verified Software 2017 - Heidelberg, Germany
Duration: 22 Jul 201723 Jul 2017
Conference number: 9
https://vstte17.lri.fr/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume10712

Conference

Conference9th Working Conference on Verified Software 2017
Abbreviated titleVSTTE 2017
CountryGermany
CityHeidelberg
Period22/07/1723/07/17
OtherCo-located with the 29th International Conference on Computer-Aided Verification (CAV 2017)
Internet address

Fingerprint

Algebra
Specifications
Flow control
Data storage equipment

Cite this

Oortwijn, W., Blom, S., Gurov, D., Huisman, M., & Zaharieva, M. (2017). An Abstraction Technique for Describing Concurrent Program Behaviour. In A. Paskevich, & T. Wies (Eds.), Verified Software. Theories, Tools, and Experiments: 9th International Conference, VSTTE 2017, Heidelberg, Germany, July 22-23, 2017, Revised Selected Papers (pp. 191-209). (Lecture Notes in Computer Science; Vol. 10712). Springer. DOI: 10.1007/978-3-319-72308-2_12
Oortwijn, Wytse ; Blom, Stefan ; Gurov, Dilian ; Huisman, Marieke ; Zaharieva, M./ An Abstraction Technique for Describing Concurrent Program Behaviour. Verified Software. Theories, Tools, and Experiments: 9th International Conference, VSTTE 2017, Heidelberg, Germany, July 22-23, 2017, Revised Selected Papers. editor / Andrei Paskevich ; Thomas Wies. Springer, 2017. pp. 191-209 (Lecture Notes in Computer Science).
@inproceedings{be48b3c4b0db4f709b9da518e7e7a713,
title = "An Abstraction Technique for Describing Concurrent Program Behaviour",
abstract = "This paper presents a technique to reason about functional properties of shared-memory concurrent software by means of abstraction. The abstract behaviour of the program is described using process algebras. In the program we indicate which concrete atomic steps correspond to the actions that are used in the process algebra term. Each action comes with a specification that describes its effect on the shared state. Program logics are used to show that the concrete program steps adhere to this specification. Separately, we also use program logics to prove that the program behaves as described by the process algebra term. Finally, via process algebraic reasoning we derive properties that hold for the program from its abstraction. This technique allows reasoning about the behaviour of highly concurrent, non-deterministic and possibly non-terminating programs. The paper discusses various verification examples to illustrate our approach. The verification technique is implemented as part of the VerCors toolset. We demonstrate that our technique is capable of verifying data- and control-flow properties that are hard to verify with alternative approaches, especially with mechanised tool support.",
author = "Wytse Oortwijn and Stefan Blom and Dilian Gurov and Marieke Huisman and M. Zaharieva",
year = "2017",
doi = "10.1007/978-3-319-72308-2_12",
language = "English",
isbn = "978-3-319-72307-5",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "191--209",
editor = "Andrei Paskevich and Thomas Wies",
booktitle = "Verified Software. Theories, Tools, and Experiments",

}

Oortwijn, W, Blom, S, Gurov, D, Huisman, M & Zaharieva, M 2017, An Abstraction Technique for Describing Concurrent Program Behaviour. in A Paskevich & T Wies (eds), Verified Software. Theories, Tools, and Experiments: 9th International Conference, VSTTE 2017, Heidelberg, Germany, July 22-23, 2017, Revised Selected Papers. Lecture Notes in Computer Science, vol. 10712, Springer, pp. 191-209, 9th Working Conference on Verified Software 2017, Heidelberg, Germany, 22/07/17. DOI: 10.1007/978-3-319-72308-2_12

An Abstraction Technique for Describing Concurrent Program Behaviour. / Oortwijn, Wytse; Blom, Stefan; Gurov, Dilian; Huisman, Marieke; Zaharieva, M.

Verified Software. Theories, Tools, and Experiments: 9th International Conference, VSTTE 2017, Heidelberg, Germany, July 22-23, 2017, Revised Selected Papers. ed. / Andrei Paskevich; Thomas Wies. Springer, 2017. p. 191-209 (Lecture Notes in Computer Science; Vol. 10712).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - An Abstraction Technique for Describing Concurrent Program Behaviour

AU - Oortwijn,Wytse

AU - Blom,Stefan

AU - Gurov,Dilian

AU - Huisman,Marieke

AU - Zaharieva,M.

PY - 2017

Y1 - 2017

N2 - This paper presents a technique to reason about functional properties of shared-memory concurrent software by means of abstraction. The abstract behaviour of the program is described using process algebras. In the program we indicate which concrete atomic steps correspond to the actions that are used in the process algebra term. Each action comes with a specification that describes its effect on the shared state. Program logics are used to show that the concrete program steps adhere to this specification. Separately, we also use program logics to prove that the program behaves as described by the process algebra term. Finally, via process algebraic reasoning we derive properties that hold for the program from its abstraction. This technique allows reasoning about the behaviour of highly concurrent, non-deterministic and possibly non-terminating programs. The paper discusses various verification examples to illustrate our approach. The verification technique is implemented as part of the VerCors toolset. We demonstrate that our technique is capable of verifying data- and control-flow properties that are hard to verify with alternative approaches, especially with mechanised tool support.

AB - This paper presents a technique to reason about functional properties of shared-memory concurrent software by means of abstraction. The abstract behaviour of the program is described using process algebras. In the program we indicate which concrete atomic steps correspond to the actions that are used in the process algebra term. Each action comes with a specification that describes its effect on the shared state. Program logics are used to show that the concrete program steps adhere to this specification. Separately, we also use program logics to prove that the program behaves as described by the process algebra term. Finally, via process algebraic reasoning we derive properties that hold for the program from its abstraction. This technique allows reasoning about the behaviour of highly concurrent, non-deterministic and possibly non-terminating programs. The paper discusses various verification examples to illustrate our approach. The verification technique is implemented as part of the VerCors toolset. We demonstrate that our technique is capable of verifying data- and control-flow properties that are hard to verify with alternative approaches, especially with mechanised tool support.

U2 - 10.1007/978-3-319-72308-2_12

DO - 10.1007/978-3-319-72308-2_12

M3 - Conference contribution

SN - 978-3-319-72307-5

T3 - Lecture Notes in Computer Science

SP - 191

EP - 209

BT - Verified Software. Theories, Tools, and Experiments

PB - Springer

ER -

Oortwijn W, Blom S, Gurov D, Huisman M, Zaharieva M. An Abstraction Technique for Describing Concurrent Program Behaviour. In Paskevich A, Wies T, editors, Verified Software. Theories, Tools, and Experiments: 9th International Conference, VSTTE 2017, Heidelberg, Germany, July 22-23, 2017, Revised Selected Papers. Springer. 2017. p. 191-209. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-72308-2_12