Transactional behavior verification in business process as a service configuration

Scott Bourne, Claudia Szabo, Quan Z. Sheng

Research output: Contribution to journalArticle

3 Citations (Scopus)

Abstract

Business Process as a Service (BPaaS) is an emerging type of cloud service that offers configurable and executable business processes to clients over the Internet. As BPaaS is still in early years of research, many open issues remain. Managing the configuration of BPaaS builds on areas such as software product lines and configurable business processes. The problem has concerns to consider from several perspectives, such as the different types of variable features, constraints between configuration options, and satisfying the requirements provided by the client. In our approach, we use temporal logic templates to elicit transactional requirements from clients that the configured service must adhere to. For formalizing constraints over configuration, feature models are used. To manage all these concerns during BPaaS configuration, we develop a structured process that applies formal methods while directing clients through specifying transactional requirements and selecting configurable features. The Binary Decision Diagram (BDD) analysis is then used to verify that the selected configurable features do not violate any constraints. Finally, model checking is applied to verify the configured service against the transactional requirement set. We demonstrate the feasibility of our approach with several validation scenarios and performance evaluations.

Original languageEnglish
Article number7850959
Pages (from-to)290-303
Number of pages14
JournalIEEE Transactions on Services Computing
Volume12
Issue number2
DOIs
Publication statusPublished - 1 Mar 2019

Keywords

  • Business process as a service
  • formal methods
  • model checking
  • transactional requirements
  • verification

Fingerprint Dive into the research topics of 'Transactional behavior verification in business process as a service configuration'. Together they form a unique fingerprint.

Cite this