When we adapt a non-Internet business to an Internet business we must re-engineer our business model, although the domain to which it applies remains the same. Testing the new model with respect to the original model becomes an important issue. How do we check that essential properties of the original model are preserved by a re-engineered model? We will explore the problem through a lightweight use of formality (Robertson 1998).
In this document, we choose book ordering as our domain, and construct models used in two different contexts: book ordering in a bookstore; book ordering on the Internet.
Our main concern is the problem of preserving basic properties after modelling a new business requirement and re-engineering a model:
The basic procedure of our research is first to build two models on two simplified scenarios( conventional book order and Internet book order); then we identify some basic properties which should hold in both models, serveing a common purpose in a retail book order domain; then we build the bridges to connect the basic properties to the definition of each model; then we test the models for the basic properties; finally, we consider the interpretation of the bridge, the basic properties and our test.
With the logic description in our research, we can sharpen our understanding of the problem. A proof procedure will be introduced to lead our exploration of a model check of basic properties. In a meanwhile, a rough mechanism will be introduced and used in our experiment.