Mandatory and Potential Choice: Comparing Event-B and STAIRS

Abstract

In order to decide whether a software system fulfills a specification, or whether a detailed specification preserves the properties of a more abstract specification, we need an understanding of what it means for one specification to fulfill another specification. This is particularly important when the specification contains one or more operators for expressing choice. Operators for choice have been studied for more than three decades within the field of formal methods in general, and within methods for action-refinement in particular. In this paper we focus on Event-B, a more recent method for action refinement. The STAIRS method belongs to another tradition. It originates from the UML community and is designed to provide an understanding of refinement and fulfillment for UML. STAIRS distinguishes between potential and mandatory choice, where only the latter is required to by preserved by refinement. This paper investigates the relationship between the operators for choice in Event-B and STAIRS.