Semantic Criteria for Choosing a Language for Big-Step Models

With the popularity of model-driven methodologies, and the abundance of modelling languages, a major question for a requirements engineer is: which language is suitable for modelling a system under study? We address this question from a semantic point-of-view for big-step modelling languages (BSMLs). BSMLs are a class of popular behavioural modelling languages in which a model can respond to an input by executing multiple, possibly concurrent, transitions. We deconstruct the operational semantics of a large class of BSMLs into high-level, orthogonal semantic aspects, and analyze the relative advantages and disadvantages of the common semantic options for each of these aspects. Our goal is to empower a requirements engineer to compare and choose an appropriate BSML.