Abstract: The temporal logic language （TLL） XYZ/E can represent both dynamic semantics and static semantic under a unified logical framework and carry out the smooth transition from the abstract specification to execuable program. This paper builds up the Certifica

Key words: XYZ/E, Certification authority, Registry authority, Describe, Refinement