In this paper, we present a framework for formal modeling and verification of service-based business processes with focus on their compliance to external regulations such as Segregation of Duties (SoD) or privacy protection policies. In our framework, control/data flow is modeled using the exogenous coordination language Reo. Reo process models are designed from scratch or (semi-)automatically obtained from BPMN, UML or WS-BPEL specifications. Constraint automata (CA), a semantic model for Reo, provide state-based representations of process workflows and enable their verification by means of model checking technology. Various extensions of CA make it possible to analyze time-, resource- and Quality-of-Service (QoS) process models.
Additional Metadata
THEME Software (theme 1)
Publisher Springer
Series Lecture Notes in Computer Science
Conference International Symposium on Formal Methods for Components and Objects
Citation
Kokash, N, & Arbab, F. (2009). Formal Behavioral Modeling and Compliance Analysis for Service-Oriented Systems. In Formal Methods for Components and Objects, 7th International Symposium (FMCO) (pp. 21–41). Springer.