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.