Refining Action Systems within B-Tool

Marina Walden, Kaisa Sere

Research output: Chapter in Book/Conference proceedingConference contributionScientificpeer-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 languageEnglish
Title of host publicationProceedings of Formal Methods Europe (FME'96)
Subtitle of host publicationSymposium on Industrial Benefit and Advances in Formal Methods
Place of PublicationOxford, England
PublisherSpringer Verlag
Pages84-103
Publication statusPublished - 1996
MoE publication typeA4 Article in a conference publication

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume1051

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

Cite this