Formalization and proof of design guidelines within the scope of testing formally specified electronic product catalogues
H. Fritzsche, T. Michel · Interacting with Computers · 2000
Electronic product catalogues (EPCs) are a class of complex event driven multimedia information systems. A software engineering model was developed in the EPK-fix project to construct and test EPCs on the basis of formal specifications. With reference to the specification a whitebox-based test technology is supported by a test assistant. The dynamic analysis prerequisites the production of an interpretable dynamic model to simulate states and transitions of an EPC discretely. A test agent controls both the model and the EPC. Formal proof techniques are employed to detect violations against formalized design guidelines. Both formulation and formalization of design rules are demonstrated by example. A horn clause interpreter is used to prove the observance of design rules in state configurations of the EPC. Error detection by formal proofs enhances the test process.