Using Linear Logic to Verify Requirement Scenarios in SOA Models based on Interorganizational WorkFlow Nets Relaxed Sound

Kênia Santos de Oliveira, Vinícius Ferreira de Oliveira, Stéphane Julia

2017

Abstract

This paper presents a method for requirement verification in Service-Oriented Architecture (SOA) models based on Interorganizational WorkFlow nets which are not necessarily deadlock-freeness. In this method, a requirement model corresponds to a public model that only specify tasks which are of interest of all parties involved. An architectural model is considered as a set of private processes that interact through asynchronous communication mechanisms in order to produce the services specified in the corresponding requirement model. Services can be seen as scenarios of WorkFlow nets. For each scenario that exists in the requirement model a proof tree of Linear Logic can be produced, and for each scenario correctly finalized, a precedence graph that specifies the task sequence can be derived. For each scenario of the architectural model, similar precedence graphs can be produced. The precedence graphs of the requirement and architectural model are then compared in order to verify if all existing scenarios of the requirement model also exist at the architectural model level. The comparison of behavior between distinct discrete events models is based on the notion of branching bisimilarity that prove behavioral equivalence between distinct finite automata. The example used to illustrate the proposed approach, shows that the method can be effective to identify if a SOA-based system satisfy the business needs specified by a model of public requirements.

Paper Citation

in Harvard Style

Oliveira K., Ferreira de Oliveira V. and Julia S. (2017). Using Linear Logic to Verify Requirement Scenarios in SOA Models based on Interorganizational WorkFlow Nets Relaxed Sound . In Proceedings of the 19th International Conference on Enterprise Information Systems - Volume 2: ICEIS, ISBN 978-989-758-248-6, pages 254-262. DOI: 10.5220/0006290202540262

in Bibtex Style

@conference{iceis17,
author={Kênia Santos de Oliveira and Vinícius Ferreira de Oliveira and Stéphane Julia},
title={Using Linear Logic to Verify Requirement Scenarios in SOA Models based on Interorganizational WorkFlow Nets Relaxed Sound},
booktitle={Proceedings of the 19th International Conference on Enterprise Information Systems - Volume 2: ICEIS,},
year={2017},
pages={254-262},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0006290202540262},
isbn={978-989-758-248-6},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 19th International Conference on Enterprise Information Systems - Volume 2: ICEIS,
TI - Using Linear Logic to Verify Requirement Scenarios in SOA Models based on Interorganizational WorkFlow Nets Relaxed Sound
SN - 978-989-758-248-6
AU - Oliveira K.
AU - Ferreira de Oliveira V.
AU - Julia S.
PY - 2017
SP - 254
EP - 262
DO - 10.5220/0006290202540262