کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
550663 | 872671 | 2006 | 16 صفحه PDF | دانلود رایگان |

This paper addresses the graphical representation of the behaviour of B specifications, using state transition diagrams. These diagrams can help understand the specification for stakeholders who are not familiar with the B method, such as customers or certification authorities. The paper first discusses the principles of the graphical representation on a deterministic example, featuring a small set of states. It then discusses the representation of specifications which feature a large or infinite set of states, or which are non-deterministic. Abstraction techniques are used to overcome these difficulties. They result in a variety of possible representations. Finally, three techniques, based on animation and proof, are presented to help construct the diagrams.
Journal: Information and Software Technology - Volume 48, Issue 3, March 2006, Pages 154–169