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 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.