A formal approach supporting the specification and verification of business conversation requirements.

How to verify adaptable business conversations during the requirements engineering process is still an open issue, especially when conversation requirements are translated into a network of cooperating e-services. Model checking is a suitable technique to address this problem. However, since requirements engineers typically adopt less theoretical models, model checking is given little attention. In this paper, we propose a statecharts-like model that supports the specification of business conversation requirements. These requirements are expressed as quality of service (QoS) and structural properties related to the flow of actions implemented by each cooperating partner. This flow is partly standard and partly exceptional. The exceptional flow specifies how conversations should adapt their behavior as a consequence of violations of QoS constraints. Moreover, the paper shows that this specification can be formally defined through a predicative time-bounded automaton which, in turn, can be translated into Promela, the input language of the SPIN model checker. A case study is discussed to show the application of the model.