A logic database for validating system models

In order to prove properties of inforrnation systerns, we need a forrnalism for representing the systern, a set of construetion rules for the appropriate CIMS of systern and a suitable environment for testing the proof. This paper builds on earlier work on the Extended Transition Network (ETN) formalism and proposes some generic construction rules for information systems specified using ETN. Ve dernonsttate that deductive databases are suitable for expressing these rules and validating ETN models by presenting our implernentation in the Iogic database GEDBLOG.