A Formal Approach for the Iterative Design of Behavioural Models

In the process of specifying update operations of an information system, it is critical to ensure that the resulting design is consistent with the developers´ understanding about the requirements, before it is adapted to a chosen platform of implementation. We present a formal approach to testing behavioral specifications that characterise the intended effects on the state as two-state, first-order predicates. By supplying use-case scenarios that are of interest, the developers are able to examine the test results, decide if the model under test is consistent, and revise the source specifications if necessary. To facilitate an iterative process of this, in this paper we develop a list of equivalence and refinement (rewriting) laws of predicates that are targeted at information system states. Our development is built upon the formal semantics and logical properties of a formal language of substitutions that serves as an abstract implementation language for these predicates.