Testing Conceptual Schema Satisfiability - Intentional Perspectives on Information Systems Engineering - page 272

entity and relationship type of the schema may have a non-empty population at
certain time. An entity or relationship type is unsatisfiable when the set of con-
straints defined in the schema can only be satisfied if the population of that type is
empty. Behaviorally, a conceptual schema is satisfiable if each event type is satisfi-
able, that is, there is at least one consistent state of the Information Base (IB) and
one event of that type with a set of characteristics such that the event constraints
are satisfied, and the effects of the event leave the IB in a state that is consistent
and satisfies the event postconditions. A state of the IB is consistent if it satisfies all
integrity constraints.
There has been a lot of work on automated reasoning procedures for check-
ing satisfiability, mainly for the structural part of a schema (a representative set
of recent papers is [1, 3, 5, 7, 8, 10, 18, 19] ). However, it is well known that
the problem of reasoning in conceptual schemas including general integrity con-
straints, derivation rules and event pre and postconditions is undecidable. Therefore,
the available automated reasoning procedures are restricted to certain kinds of con-
straints, derivation rules, pre/postconditions or domains, or they may not terminate
in some circumstances.
In this chapter, we explore an alternative approach to satisfiability checking,
which can be used when conceptual schemas are developed in the context of a
development environment that allows their testing. Essentially, this means that there
is a testing language, in which the conceptual modeler writes programs that test a
conceptual schema, and a test processor, which is a program able to execute test
programs and report on their result.
The main contribution of this chapter is to show that when conceptual schemas
can be tested then their satisfiability can be proved by testing. The idea is that the
conceptual modeler sets up a test case such that if its verdict is Pass then by defini-
tion the entity or relationship or event type under test is satisfiable. If the conceptual
modeler is unable to set up such test case, then this is not formal proof of unsatisfia-
bility. We show that the unsatisfiability results obtained by testing are not as strong
as those obtained by automated reasoning procedures when they are applicable, but
in many practical cases testing provides a clue that helps to uncover a faulty schema.
The idea that satisfiability can be proved by testing is similar to that of validating
a conceptual schema by prototyping, as was already proposed in the work of the
TODOS project [ 16] . In both cases the main intention is similar: ensuring the cor-
rectness of the conceptual schema. The means are only slightly different: in testing
we assume that the conceptual schema is directly executable, while in prototyp-
ing it is assumed that the prototype is automatically generated from the conceptual
schema.
The structure of the chapter is as follows. In the next section, we briefly review
the main concepts and the notation used to define conceptual schemas. We also
review the main characteristics of test kinds, test cases and test programs needed in
this chapter. In Sect. 3 we describe how to test the satisfiability of entity, relationship
and domain event types, with examples taken from a fragment of the conceptual
schema of the osCommerce system [ 24] , a popular industrial e-commerce sys-
tem. All of the examples in this chapter are taken from this case study. The full