Formalisation of Requirements with emphasise on Feature Interaction detection

this paper a framework, Tussilago , for the specification of telephone services is presented. We particularly address the following problems. 1. Formalisation in a way close to the intuitive understanding of a set of requirements expressible with use cases. Our formalism uses a particular interpretation of Message Sequence Charts (MSC), where the graphical syntax used to visualise MSCs has a close relationship to the specification. 2. Structuring formal specifications of telephone services into modules might be used to increase reusability of specifications. New modules might also cause addition of new functionality. A non-monotonic construct introduced to combine modules will further increase reusability of specifications. 3. Automatic detection of a class of interactions between features. We show how a method described in [2] can be directly used on the presented framework. We aim for a specification style, in which each feature is specified in a separate module. Ideally, a complete telephone service should be obtainable by composing a module containing a basic service with those modules that specify the desired set of features. We assume a system modelled as a set of individuals where the state of the system is defined by the state of individuals and relations between them. As individuals are distributed in a network, the global state might be seen as the composition of local states of the individuals. The local state of an individual might for example reflect that it is connected with some other individual. Stimuli from the environment are modelled by external events. For example, a user dialling a number is such stimuli to an individual in the system. But the effect of dialling is not isolated to one individual as it triggers a request to connect to another individ..