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

Testing Conceptual Schema Satisfiability

Antoni Olivé and Albert Tort

Abstract Satisfiability is one of the properties that all conceptual schemas must
have. Satisfiability applies to both the structural and the behavioral parts of a concep-
tual schema. Structurally, a conceptual schema is satisfiable if each base or derived
entity and relationship type of the schema may have a non-empty population at
certain time. Behaviorally, a conceptual schema is satisfiable if for each event type
there is at least one consistent state of the information base 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 information base in a state that is consistent and
satisfies the event postconditions. There has been a lot of work on automated rea-
soning procedures for checking satisfiability but it is well known that the problem of
reasoning with integrity constraints and derivation rules in its full generality is unde-
cidable. In this chapter, we explore an alternative approach to satisfiability checking,
which can be used when conceptual schemas are developed in the context of an envi-
ronment that allows their testing. The main contribution of this chapter is to show
that when conceptual schemas can be tested then their satisfiability can be proved
by testing.

1 Introduction

A conceptual schema of an information system is correct if the knowledge that it
defines is true for the domain and relevant to the functions that the system must
perform [ 11] . The correctness of a conceptual schema must be checked during the
requirements validation phase [ 16, 20- 23, 27] .
Satisfiability is one of the properties that all correct conceptual schemas must
have. Satisfiability applies to both the structural and the behavioral parts of a concep-
tual schema. Structurally, a conceptual schema is satisfiable if each base or derived