Design Methods, Component-based Stepwise Refinement Process

Software Architecture has been a hot research field in Software Engineering. This kind of method focuses on the overall organization of software system. It studies the interrelationships between components in an abstract level, therefore understands and analyses the behaviors and properties of the whole system in an overall and integrated view. It is very useful to develop large complex software.A question that frequently arises for architectural design is "How can I implement a system from a high-level architectural design to the low-level architectural design and eventually the final executable program?" This Problem involves architectural refinement methods. It's very important to assure the correctness of each refinement step. And this is also our purpose in this thesis.Instead of refining an architectural design by another different style design in whole, Stepwise refinement programming design method based on components refines an architectural design by replacing a component's static semantics by its dynamic semantics. Because XYZ/E can represent static and dynamic semantics in a uniform frame, the transition from the specification of the component to its corresponding architecture structure designed at that step can be formally validated. The correctness of refinement can be verified by the tool XYZ/VERI based on Hoare logic ruls and verifying methods of temporal logic.In the thesis we first describe how to formalize components, connecters and architecture styles using temporal logic programming language XYZ/E. Then it presents the programming method based on components and stepwise refinements from static semantics to dynamic semantics. This method combined software architecture and XYZ system effectively. Briefly, the process of programming bythis methods includes: write specifications for the components according software requirements, select the proper architecture style, build sub-components and connectors, configure corresponding preferences, then create XYZ/E program, check the consistency of this program and the specification of the component. In this way, it assures that every refinement step is safe and correct. Do the same to the following sub-components, until there's no static description but dynamic semantics.The advantage of this method is that it can find the errors in program earlier and therefore reduce the development cost. The drawback is that there are not any well-perform automatic tools for verif~'ing the correctness of refinement yet.