73. Requirement Verification in SOA Models Based on Interorganizational WorkFlow Nets and Linear Logic

This paper presents a method for requirement verification in Service-Oriented Architecture (SOA) models based on Interorganizational WorkFlow nets. In SOA Design, a requirement model (public model) only specify tasks which are of interest of all parties involved in the corresponding interorganizational architectural model (a set of interacting private models). Architectural models involve much more tasks: they contain the detailed tasks of all the private processes (individual workflow processes) that interact through asynchronous communication mechanisms in order to produce the services specified in the requirement model. In the proposed approach, services correspond to scenarios of Interorganizational WorkFlow nets. For each scenario of the public and private models, a proof tree of Linear Logic is produced and transform into a precedence graph that specifies task sequence requirements. Precedence graphs of the public and private models are then compared in order to verify if all the existing scenario of the requirement model also exist in the architectural model. The comparison of the models (public to private) is based on the notion of branching bisimilarity that prove behavioral equivalence between distinct finite automatas.