Formal Behavioral Modeling and Compliance Analysis for Service-Oriented Systems
Presented at the International Symposium on Formal Methods for Components and Objects
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.
|THEME||Software (theme 1)|
|Series||Lecture Notes in Computer Science|
|Conference||International Symposium on Formal Methods for Components and Objects|
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.