Static function hierarchies and models of the dynamic behaviour are typically used in e-commerce systems. Issues to be verifies are the completeness and correctness of the static function hierarchies, business rules valid in defined business domains and the consistency of models on different levels of abstraction. Today the systems are mostly tested manually. Automated support may the verification of static dependencies modelled in Boolean logic. Moreover, the checking of dynamic process models can be supported by temporal logic specifications and model checking tools.
Most large scale commercial systems share similar modelling and architecture concepts. e-Commerce systems like Intershop Enfinity are typical examples of this type of systems. Moreover other commercial e.g. the ERP system SAP R/3 have the same modelling characteristics based on business processes. The design is modelled on different abstraction levels. The static dependencies between the functionality are modelled in hierarchies. The dynamic interactions are designed in process and workflow models.
A typical modelling method for commercial systems in general is ARIS (Architecture integrated Information Systems) supported by the ARIS tool set of IDS Scheer (a closer description of a ARIS subsystem optimised for e-commerce is given in section 2). The typical problems that arise from this modelling concept are: • Static function hierarchies must be complete and correct. • Specific business rules, which are valid in defined business domains, are to be kept. • Dynamic models on different levels of abstraction must be consistent. Current practice is to test and check systems manually. Besides specific rules and regulations, experiences are used as base. However, it is obvious that the manual tests do not cover all possible errors. Additionally they are very cost intensive especially for commercial software developers.
As already mentioned the ARIS modelling concept is used in commercial systems in
general. In this section we will present ARIS for Enfinity [
(generic model)
(proprietary model ARIS for Enfinity) However the ARIS for Enfinity modelling concept must still be considered as a very generic model for e-commerce systems and may be applied for other systems e.g. like mySAP. As there exist no final standards in e-commerce modelling (currently on base of Web Services and BPEL4WS first approaches towards standardisation are in progress) ARIS for Enfinity already gives a clear outlook on the future standard. Since there are clear parallels between future BPEL4WS modelling and the already successfully applied ARIS for Enfinity, this paper is based on the ARIS for Enfinity experiences.
ARIS for Enfinity supports four layers of abstraction. The layers one to three are
standard in large scaled-commerce systems and other commercial applications. Only
the fourth layer uses an Enfinity specific model presentation (Intershop Pipelines).
However the basic concept is also base of generic modelling like in BPEL4WS, which
bears considerable similarities to the Intershop Pipelines.
1. Business Scenarios define the basic core, coarse grain elements of the e-commerce
application. They are very abstract. The verification on this level is and will be done
by human experts. Automation is not desirable.
2. Business Process Overview provides the overview over the functionality (main
functions). Usually only the static relations of the functions are considered
(function hierarchies).
3. Business Processes describe the dynamic processes in the system. Yet, the models
are abstract. However, the business process models may be refined to the concrete
workflows. Usually EPCs (Event-driven Process Chains, [
The different ARIS model types are depicted in table 1. The Function Hierarchy shows which function is member of which other function.
The dynamic model Event-driven Process Chain is a rather abstract process description. The main elements are the functions (rounded rectangles) and the events (hexagons) which are connected by the organisational flow (arrows) and the logic connectors (Boolean AND as depicted as well as OR and XOR). Examples of further elements are organisational units executing certain functions, deliveries or application systems providing functions.
The Intershop Pipeline Models include different types of nodes: Pipelet nodes implement the re-usable specific business function. This business function is realised by a small Java class. For more complex operations these classes call library code (in the persistence layer), e.g. access to data bases or other systems. Control nodes define the control flow of Pipelines. An example in the table is the call of a Sub-Pipeline or the termination of this Sub-Pipeline. The interaction of the Pipelines and the web pages (templates) exported to the web clients is described in interaction nodes. These nodes define which data a Pipeline receives from a template activating the Pipeline (start interaction) and which data is delivered to the resulting template (interaction).
<<CarletedrintaCtiavred>> <<PaaltyerbnyatBiviell>> P<a<yalotenrnative>>
Delivery
O<r<dceornPcreopct>es>s <<weak Constraint>>
mutex <<requires>> <<mutex>>
The static function hierarchies are rather easy to verify. The configurations of functions
may be represented by Boolean formulae [
The more interesting question is how to visualise the hierarchy. One possibility may be to extend the ARIS model. Another alternative is to apply a more complex model. UML class models may serve as compromise. They support numerous expressive modelling elements and can be exported from the ARIS tools.
Besides the ordinary inclusion relationship (represented by aggregation) there exist variability (inheritance). Functions may be mandatory (AND), optional (OR) or alternative (XOR). Moreover cross-tree constraints are introduced (either both functions required or are mutual exclusive).
Typical rules on the level of static function hierarchies are: • The number of times specific functions have to occur. E.g. a web-shop does not support all types of payment or delivery which are potentially possible. • The locations in the hierarchy, where functions or sub-hierarchies of functions are placed, are relevant.
Depending on the specific application type (called solution) like business to business (B2B), business to consumer (B2C) or e-procurement there are variants (considered as rules) in the characteristic hierarchies, e.g. B2C and e-procurement solutions offer a comparatively large, predefined sub-hierarchy of price management functions while B2B solutions support only a single function.
Fig. 2. Example: Login and Presentation Process
At Intershop a set of business rules (best practices) have been collected. Usually these rules are base of the manual testing. Figure 2 shows a business process to be verified. This process describes the login and identification of a customer and the resulting different purchase and presentation functions. In contrast to the most other process models the chosen example is quite small and easy to overlook. Usually the models are much larger.
These rules, which have to be verified, deal with the temporal dependencies.
Therefore they can be transformed in temporal logic. In our case we apply Computational
Tree Logic (CTL) which is supported by the model checking tool Symbolic Model
Validation (SMV) [
AG(Customer is on Home Page -> AG(!Customer Data Check)) Again, we start with the same assumption as in the first example (Customer is on Home P age = ).
The results of the SMV model checker are shown in figure 3.
Further examples for best practices / business rules are: • Before a customer pays always a product presentation page is shown. • There is no path which leads to an unintended loss of the content in the customer’s shopping cart. • The customer’s order may be identified in the different subsystems (ERP, logistic system or e-commerce system).
There are no typical rules for the refinement of more abstract models (e.g. EPC models)
to more detailed ones (e.g. Pipelines or BPEL4WS). However, usually characteristic
sequences in abstract models should appear in detailed models. These characteristic
sequences may serve as specifications, which have to be verified. These sequences may
be considered as a rules which are then checked as demonstrated in section 3.2.
However up to now there is little research how to manage this kind of very specific rules
which are different for each application. The versioning approach for static features
like presented in [
In hardware verification there are a considerable number of model checking approaches.
The verification of software and specifically the dynamic processes is still at it’s very
beginning. An early example for software checking is Bandera, an integrated collection
of program analysis and transformation components [
Assuming the system is developed starting with manually produced state charts (as
realised in [
The validation of the behaviour of components is also related to this work since it
meets the problems in the lower abstraction levels. In [
Some approaches deal with the validation of workflows in general by applying
model checkers. An example for a workflow checking approach is [
The testing of large scale commercial systems such as e-commerce systems is currently manually realised. Function hierarchies may be modelled in Boolean logic which are automatically verified by theorem proofer or with term rewriting. The checking of dynamic process models (e.g. against business rules) can be supported by temporal logic and model checking techniques.
Future work will be to improve the workflow models on the most detailed level. Further semantic information has to be captured. Code characteristics of the Pipelets will be included in the models.
Another issue is the improvement of the model checking technology. Since the SMV is quite optimal for the representation of hardware, the support of workflows and software requires new verification systems to be invented. Specifically properties (e.g. representing further semantics) and their hierarchical arrangement have to be dealt with.