UML activity diagrams can be used to model business processes which are implemented in a software project. It is a worthwhile goal to automatically transform at least parts of UML diagrams into software. Automated code generation reduces the total amount of errors in a software project but the model itself can still violate specified requirements. A quality improvement is the usage of a model checker which searches through the whole state space of model and checks whether all requirements are met. A model checker requires a formal description of a model for a complete verification. Activity diagrams often describe processes informally which is difficult to verify with a model checker. We therefore propose the transformation of activity to statechart diagrams which allow a more detailed and formal description. Several algorithms exist to map UML statecharts into a model checker input language for a successful formal verification. Afterwards, the model checker searches through the whole state space of a statechart and therefore has to store each state in memory. UML statecharts can reach a high degree of complexity which is problematic for a complete state space traversal because the total amount of available memory is exhausted. Accordingly, we present the domain specific language UDL (UML Statechart Modeling Language) and a transformation from UDL into the Spin model checker input language Promela. UDL contains features for property preserving abstraction which reduces the models state space and therefore the memory consumption of a model checker. Furthermore, we introduce an optimisation technique for the transformation process from UDL to Promela which focuses on a reduced model checker run-time. A case study with a movement tracking system demonstrates how our approach could significantly reduce the memory consumption of a model checker and allows the verification of complex models.

Compliance management is a critical concern for corporations, required to respect contracts. This concern is particularly relevant in the context of business process management (BPM) as this paradigm is getting adopted more widely for designing and building IT systems. Enforcing contractual compliance needs to be modeled at different levels of a BPM framework, which also includes the service layer. In this paper, we discuss requirements and methods for modeling contractual compliance for a SOA-supported BPM. We also show how business rule management integrated into an industry BPM tool allows modeling and processing functional and non-functional-property constraints which may be extracted from business process contracts. This work proposes a framework that responds to the requirements identified and proposes an architecture implementing it. Our approach is also illustrated by an example.

Requirement elicitation is one of the earliest phases of a requirement engineering lifecycle. However, even though years of research have gone into seeking machine support for requirements engineering, the methods used are still highly manual and the vision of automatic transfer of business analysis requirements into IT systems supporting the business is still far from reach. On the other hand, incepting knowledge for creating AS-IS business processes in enterprise models has been recognized as a hard problem. In the context of a process centric organization, we propose an approach to create AS-IS business process models by automatically transferring requirements to the business process layer. Our aim is to enable carrying business requirements, goals and policies from an inception layer to the operational business process management layer. We place our research in the context of a semantic business process management platform (SUPER) as the support to exploit the output of our research. This paper grounds this research work and proposes a research design for requirement elicitation for producing early-phase business process models that are nearer to the business analysis layer.

Models of commercial systems reflect either the statical structure or the dynamic behavior of a system. The dynamic aspects are the business processes and their models. Whereas the static relations in a system may be expressed by Boolean logic, the dynamic activities and their temporal sequences ask for a better formalism, e.g. temporal logic. Temporal logic is based on Boolean logic extended by operators expressing the temporal order of states. In general there are different technologies to verify temporal sequences. Our choice is the model checking concept. In the paper we present examples of business process models and how these models may be checked. We introduce a model to specify the rules (rules model) and demonstrate how the results of the checks can be displayed in the business process models. These models and the rules are represented in a graphical editor. Both models are transformed into a formal language which may be processed by a verification tool - a model checker in our case. The results are then visualized in the graphical editor indicating where the model violates or keeps the rules.

Compliance management, risk analysis, and auditing are disciplines that are critical for large scale distributed enterprise systems. The way these complex systems are developed and deployed makes the management and enforcement of enterprise goals or policies a hard task. This is also true for compliance management of business processes (BPs). Such an observation is emphasized if we give compliance management the scope of the whole enterprise model. In this paper we explain our approach to modeling compliance measures based on policies and present a framework for managing and enforcing compliance policies on enterprise models and BPs. We discuss our ideas in the context of a semantically-enabled environment and discuss why leveraging compliance checking to a semantic level enhances compliance management.

Processes count to the most important assets of companies. Ensuring the compliance of processes to legal regulations, governance guidelines, and strategic business requirements is a sine qua non condition to controlling business behavior. Implementing business process compliance requires means for modeling and enforcing compliance measures. In this work, we motivate the need for automation in compliance management and introduce the role of policies. We then distinguish eight requirements for a compliance management framework. We also discuss different ways of conducting compliance checking. Finally, we propose a policy-based framework for business process compliance management. We eventually proceed to a discussion of the soundness and practicability of our approach, followed by an investigation of the main challenges ahead of our approach to policy-based semantic business process compliance management.

An essential but difficult task to achieve in distributed enterprise systems is the management and enforcement of regulations and policies. We explore and discuss ideas for the implementation of enterprise wide compliance management. We propose an approach that builds on policies to realize compliance checking on semantic descriptions of enterprise models. This paper is meant to initiate a discussion about the pro and contra of our approach.

In this paper we present our approach to model and verify workflow-intensive systems. Besides the functional properties (given by the temporal workflow description) we augment the model and model checking with additional property treatment to deal with multifarious non-functional properties and property hierarchies. This enables a more powerful verification of requirements such as given business-driven regulations in these system workflows.

The eCommerce system development of Intershop is based on different models on various levels of abstraction. The software engineering tool ARIS represents most of these models. In this paper we focus on the validation of the business process models on an intermediate abstraction level of the ARIS model. The business processes may be derived from process patterns and have to follow specific rules (best practices). The validation of the compliance with these rules and the consistency with the original business process pattern is the focus of this paper.

This paper presents an approach to ensure correctness of composed systems. It takes into consideration that correctness can usually be achieved only to a certain degree (except for some small and very mission-critical applications) and complete specifications are usually not practicable. By modelling the parts, the composition activities and the requirements specification we automise the checking procedures using model checking. An important issue hereby is that our approach allows partial modelling and specification. Workshop web page: http://www.easycomp.org/sc2002

Requirements that have a cross-cutting impact on software present many problems for software development throughout the lifecycle. Aspect Oriented Programming (AOP) and related techniques propose solutions to this problem. These language extensions are usually implemented by providing a weaver that reimplements major parts of a compiler and thus has a large code base. This paper proposes to define XML “operators” and to work on XML representations of abstract syntax trees (AST) for the base language that can be generated by modifying a conventional compiler with relative ease.

Feature interaction is nothing new and not limited to computer science. The problem of undesirable feature interaction (feature interaction problem) has already been investigated in the telecommunication domain. Our goal is the investigation of feature interaction in component-based systems beyond telecommunication. The position paper outlines terminology definitions. It proposes a classification to compare different types of feature interaction. A list of examples give an impression about the nature and the importance of feature interaction.

Component-based approaches for the software development are well-known. Most of these approaches (like CORBA and COM++) focus on the realization of the connection between the components and their interactions. In this paper we concentrate on the missing items in the component-based software engineering: the problem how to model component composition and to validate them. We apply the component model based on the interface description with InPorts and OutPorts which allow a rather detailed definition of the components interaction. Moreover we take the term feature to name the core requirements to a component. Features are used to drive the description of the component composition which is regarded as an combination of features expressed by logical operators. Moreover the InPorts and OutPorts describe the dynamic component interactions. The combination of OutPorts and InPorts according to the component composition rules allows to reason about the component system's dynamic behavior.

Various recent approaches aim at improving the application of the separation of concerns principle by introducing new system units. Although they seem to have the potential to improve the system development process, additional challenges evolve. This paper addresses some challenges concerning the reusability of these new system units. Our considerations about reusability are twofold. First, the independence of these system units is regarded on the mechanism level. Second, the composition validation problem emerging from the composition of these new and also reusable system units is investigated. The problems are illustrated by means of two examples.