Refining Action Systems within B-Tool

Marina Waldén; Kaisa Sere

doi:10.1007/3-540-60973-3_82

Refining Action Systems within B-Tool

Marina Waldén, Kaisa Sere

Information Technology

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

11 Citations (Scopus)

Abstract

Action systems is a formalism designed for the construction of parallel and distributed systems in a stepwise manner within the refinement calculus. In this paper we show how action systems can be derived and refined within a mechanical proof tool, the B-Tool. We describe how action systems are embedded in B-Tool. Due to this embedding we can now develop parallel and distributed systems within the B-Tool. We also show how a typical and nontrivial refinement rule, the superposition refinement rule, is formalized and applied on action systems within B-Tool. A derivation towards a distributed load balancing algorithm is given as a case study.

Original language	English
Title of host publication	FME '96: Industrial Benefit and Advances in Formal Methods
Subtitle of host publication	Third International Symposium of Formal Methods Europe Co-Sponsored by IFIP WG 14.3, Oxford, UK, March 18 - 22, 1996. Proceedings
Place of Publication	Oxford, England
Publisher	Springer Verlag
Pages	84-103
ISBN (Print)	978-3-540-60973-5
DOIs	https://doi.org/10.1007/3-540-60973-3_82
Publication status	Published - 1996
MoE publication type	A4 Article in a conference publication

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
Volume	1051

Access to Document

10.1007/3-540-60973-3_82

Cite this

Waldén, M., & Sere, K. (1996). Refining Action Systems within B-Tool. In FME '96: Industrial Benefit and Advances in Formal Methods: Third International Symposium of Formal Methods Europe Co-Sponsored by IFIP WG 14.3, Oxford, UK, March 18 - 22, 1996. Proceedings (pp. 84-103). (Lecture Notes in Computer Science; Vol. 1051). Springer Verlag. https://doi.org/10.1007/3-540-60973-3_82

@inproceedings{1c4dfc2449114e79b742a8968196ee8b,

title = "Refining Action Systems within B-Tool",

abstract = "Action systems is a formalism designed for the construction of parallel and distributed systems in a stepwise manner within the refinement calculus. In this paper we show how action systems can be derived and refined within a mechanical proof tool, the B-Tool. We describe how action systems are embedded in B-Tool. Due to this embedding we can now develop parallel and distributed systems within the B-Tool. We also show how a typical and nontrivial refinement rule, the superposition refinement rule, is formalized and applied on action systems within B-Tool. A derivation towards a distributed load balancing algorithm is given as a case study.",

author = "Marina Wald{\'e}n and Kaisa Sere",

year = "1996",

doi = "10.1007/3-540-60973-3_82",

language = "English",

isbn = "978-3-540-60973-5",

series = "Lecture Notes in Computer Science",

publisher = "Springer Verlag",

pages = "84--103",

booktitle = "FME '96: Industrial Benefit and Advances in Formal Methods",

}

Waldén, M & Sere, K 1996, Refining Action Systems within B-Tool. in FME '96: Industrial Benefit and Advances in Formal Methods: Third International Symposium of Formal Methods Europe Co-Sponsored by IFIP WG 14.3, Oxford, UK, March 18 - 22, 1996. Proceedings. Lecture Notes in Computer Science, vol. 1051, Springer Verlag, Oxford, England, pp. 84-103. https://doi.org/10.1007/3-540-60973-3_82

Refining Action Systems within B-Tool. / Waldén, Marina; Sere, Kaisa.
FME '96: Industrial Benefit and Advances in Formal Methods: Third International Symposium of Formal Methods Europe Co-Sponsored by IFIP WG 14.3, Oxford, UK, March 18 - 22, 1996. Proceedings. Oxford, England: Springer Verlag, 1996. p. 84-103 (Lecture Notes in Computer Science; Vol. 1051).

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

TY - GEN

T1 - Refining Action Systems within B-Tool

AU - Waldén, Marina

AU - Sere, Kaisa

PY - 1996

Y1 - 1996

N2 - Action systems is a formalism designed for the construction of parallel and distributed systems in a stepwise manner within the refinement calculus. In this paper we show how action systems can be derived and refined within a mechanical proof tool, the B-Tool. We describe how action systems are embedded in B-Tool. Due to this embedding we can now develop parallel and distributed systems within the B-Tool. We also show how a typical and nontrivial refinement rule, the superposition refinement rule, is formalized and applied on action systems within B-Tool. A derivation towards a distributed load balancing algorithm is given as a case study.

AB - Action systems is a formalism designed for the construction of parallel and distributed systems in a stepwise manner within the refinement calculus. In this paper we show how action systems can be derived and refined within a mechanical proof tool, the B-Tool. We describe how action systems are embedded in B-Tool. Due to this embedding we can now develop parallel and distributed systems within the B-Tool. We also show how a typical and nontrivial refinement rule, the superposition refinement rule, is formalized and applied on action systems within B-Tool. A derivation towards a distributed load balancing algorithm is given as a case study.

U2 - 10.1007/3-540-60973-3_82

DO - 10.1007/3-540-60973-3_82

M3 - Conference contribution

SN - 978-3-540-60973-5

T3 - Lecture Notes in Computer Science

SP - 84

EP - 103

BT - FME '96: Industrial Benefit and Advances in Formal Methods

PB - Springer Verlag

CY - Oxford, England

ER -

Refining Action Systems within B-Tool

Abstract

Publication series

Access to Document

Fingerprint

Cite this