The Formalization of Open Collection System of Information Objects

In order to discover the discription properties of the research objects, we design an open system for information objects collecting over Internet. The major functions of this system include object registering, registration information querying, object information inputing, object updating, objects browsing, and so on. We formalize the system in Z notations to avoid the misunderstanding in semantics in the requirement specification. This formalization will be used in further model checking.