CSSL: a logic for specifying conditional scenarios

Abstract

Scenarios and use cases are popular means of describing the intended system behaviour. They support a variety of features and, notably, allow for two different interpretations: existential and universal. These modalities allow a progressive shift from examples to general rules about the expected system behaviour. The combination of modalities in a scenario-based specification poses technical challenges when automated reasoning is to be provided. In particular, the use of conditional existential scenarios, of which use cases with preconditions are a common example, require reasoning in branching time. Yet, formally grounded approaches to requirements engineering and industrial verification approaches shy away from branching-time logics due to their relatively unintuitive semantics.