Like other large scale systems interoperating with other systems large scale e-commerce systems and their interactions are hard to be validated or verified although the quality requirements for these systems are very high. The question is now: are there any further possibilities to check these systems except doing this manually? An approach is to focus on the models describing the systems; and specifically to focus on the models of the behavior. Although the verification of temporal aspects is much more complex than checking static dependencies there is a promising technology: model checking. Nevertheless we need distinctive improvements before this technology can be applied in the real system development. We need graphical formal requirement notations for different kinds of process model notations as representations of the specification of rules. We must be able to present the results positive and especially negative to the different types of stakeholders. And finally the model checking technique has to be improved in order to deal with different types of model elements which are typical for business process models.

Business process management (BPM) as a paradigm for enterprise planning and governance is nowadays a core discipline of information systems management. Growing up from the first process re-engineering initiatives in the 1980's, BPM technologies now seek to span all of the organizational silos of enterprises, and also expand vertically from the strategy layers where visions and goals are defined to the lower data transaction layers. Ensuring the compliance of processes to the guidance and control provided to the business by regulations is an obligation to every enterprise. In this work, we motivate the need for automation in compliance management and propose the use of policies as a modeling concept for regulations. We introduce the CASE model for structuring regulatory compliance requirements as policies. Policies shall allow to model regulations at abstraction levels adequate to implementing platform independent mechanisms for policy verification. We describe the CASE model and explain how it can be used to structure and model policies extracted from regulations. This chapter also defines a policy modeling ontology that we propose as a language for formally modeling CASE policies. The basic CASE model and the corresponding policy modeling ontology support compliance of enterprise processes to regulations by enabling automation to compliance checking (verification). The utilization of the CASE method as well as the policy ontology is showcased using an example of resource access control in business processes.