Refining Action Systems within B-Tool

Marina Walden; Kaisa Sere

Refining Action Systems within B-Tool

Marina Walden, Kaisa Sere

Information Technology

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

9 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	Proceedings of Formal Methods Europe (FME'96)
Subtitle of host publication	Symposium on Industrial Benefit and Advances in Formal Methods
Place of Publication	Oxford, England
Publisher	Springer Verlag
Pages	84-103
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

Fingerprint Dive into the research topics of 'Refining Action Systems within B-Tool'. Together they form a unique fingerprint.

Cite this

@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 Walden and Kaisa Sere",

year = "1996",

language = "English",

series = "Lecture Notes in Computer Science",

publisher = "Springer Verlag",

pages = "84--103",

booktitle = "Proceedings of Formal Methods Europe (FME'96)",

}

Refining Action Systems within B-Tool. / Walden, Marina; Sere, Kaisa.

Proceedings of Formal Methods Europe (FME'96): Symposium on Industrial Benefit and Advances in Formal Methods. 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 - Walden, 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.

M3 - Conference contribution

T3 - Lecture Notes in Computer Science

SP - 84

EP - 103

BT - Proceedings of Formal Methods Europe (FME'96)

PB - Springer Verlag

CY - Oxford, England

ER -