Research On C/S Architectural Style Based On XYZ/SE

XYZ/SE is the first temporal logic language, which is proposed by Chinesescholar Prof. Tang Zhisong after his research on formal method for over20years.Ithas a significant theoretical value and application prospect for its uniqueness.However, it is not used widely for applications and researches since it emerges.Therefore, this dissertation will study architectural style based on XYZ/SE temporallogic language.Firstly, this dissertation gives a detailed overview of the key syntax for XYZ/SE.This dissertation also proposes a common procedure for architectural descriptionbased on XYZ/SE. In the meanwhile, based on step-wise technology, the dissertationalso gives the procedure for XYZ/SE application, which is tested on TIPS. In thisapplication procedure, it begins to decompose TIPS into three subcomponents, i.e.,client component, connector component, server component and server subcomponent.Also, the TIPS as a whole is formally described in XYZ/SE. This is followed by thedescriptions of these components in XYZ/SE to ensure the consistency between theabstract level and concrete level. The results show that XYZ/SE supports well forspecification description in different abstract levels as well as the smooth transitionfrom static semantics to dynamic semantics.Secondly, this dissertation emphasizes on the research of the partial correctnessrules in XYZ/SE framework. This dissertation also proposes the general procedurefor partial correctness proof of architectural descriptions given in previous chapter.Based on the same subject TIPS, these descriptions are transformed graduallyaccording to the partial correctness rules until they reach the expected results in theuniform framework. Conclusion can be drawn that it is easy to judge visuallywhether the program has the property of partial correctness in a static way. Thiswork also shows that Hoare logic can be expressed with XYZ/SE in the uniformframework. What is more, the proposed method has the advantage of uniform offormal description and partial correctness along with the simplification of partialcorrectness proof.