2011/11/11 by Cátia Vaz, Carla Ferreira, Vaz, C. +1
Business, Management and Accounting · Computer Science · #Advanced Software Engineering Methodologies #Business Process Modeling and Analysis #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Service-Oriented Architecture and Web Services
paper · pdf · doi:10.48550/arxiv.1111.2824
openalex publication_date 2011/11/11 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
This paper proposes the use of model-checking software technology for the verification of workflows and business processes behaviour based on web services, namely the use of the SPIN model checker. Since the specification of a business process behaviour based on web services can be decomposed into patterns, it is proposed a translation of a well known collection of workflow patterns into PROMELA, the input specification language of SPIN. The use of this translation is illustrated with one business process example, which demonstrates how its translation to a PROMELA model can be useful in the web service specification and verification.