Formalization and proof of design guidelines within the scope of testing formally specified electronic product catalogues

Electronic product catalogues (EPCs) are a class of complex event driven mu ltimedia information systems. A software engineering model was developed in the EPK-fix project to construct and test EPCs on the basis of formal spec ifications. With reference to the specification a whitebox-based test techn ology is supported by a test assistant. The dynamic analysis prerequisites the production of an interpretable dynamic model to simulate states and tra nsitions of an EPC discretely. A test agent controls both the model and the EPC. Formal proof techniques are employed to detect violations against for malized design guidelines. Both formulation and formalization of design rul es are demonstrated by example. A horn clause interpreter is used to prove the observance of design rules in state configurations of the EPC. Error de tection by formal proofs enhances the test process. (C) 2000 Elsevier Scien ce B.V. All lights reserved.