Refining Action Systems within B-Tool

Marina Waldén, Kaisa Sere

Research output: Chapter in Book/Conference proceedingConference contributionScientificpeer-review

11 Citations (Scopus)


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 languageEnglish
Title of host publicationFME '96: Industrial Benefit and Advances in Formal Methods
Subtitle of host publicationThird International Symposium of Formal Methods Europe Co-Sponsored by IFIP WG 14.3, Oxford, UK, March 18 - 22, 1996. Proceedings
Place of PublicationOxford, England
PublisherSpringer Verlag
ISBN (Print)978-3-540-60973-5
Publication statusPublished - 1996
MoE publication typeA4 Article in a conference publication

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag


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

Cite this