Home
Scholarly Works
Mandatory and Potential Choice: Comparing Event-B...
Chapter

Mandatory and Potential Choice: Comparing Event-B and STAIRS

Abstract

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 be preserved by refinement. This paper investigates the relationship between the operators for choice in Event-B and STAIRS.

Authors

Johnsen E; Pun K; Steffen M; Tarifa S; Yu I

Book title

From Action Systems to Distributed Systems

Pagination

pp. 43-56

Publisher

Taylor & Francis

Publication Date

May 12, 2016

DOI

10.1201/b20053-11
View published work (Non-McMaster Users)

Contact the Experts team