Research, Analysis And Evolution Of Component Behavior Based On Formal Methods

In the process of component-based software development, component is the basic unit of the software reuse, the component evolution is composed of a series of complex changed activities. And in the process of dynamic evolution, when a component changes, it is likely to lead to some subsystems or components behavior affected which are associated with this component behavior, thus breaking some constraint conditions, at last destroy the balance of the whole system. Component as the encapsulation body released independently, the internal realization is invisible to external, and its interface is the only way that the component interacts with other components or the surrounding environment. Then from the angle of interface, this dissertation focuses on the question of component-based software dynamic evolution, gives a fine-grained component with formal method, does some research on the component behavior and other problems.The main content of this dissertation is as follows:1. Defines and describes the software system component model SCM with formal method, which is as the formal tool of abstraction and modeling to the potential evolving system. Then proposes the formalization of component interface and discusses some properties of the component interface.2. Based on the formalization of component interface, gives the definition of component behavior and analyzes the behavior relativities among the components. The analysis of component behavior relativity is from three aspects to discuss as controlled related, mutexes related and consistent related, which is according to the component composition mechanism. All of these lay the foundation for the component evolving capability analysis, the software evolution management.3. Analyses the problem of component evolution and proposes the judgment conditions of the component evolving capability, which is judged by the fairness and liveness of system. At the same time, gives the judging algorithms of these two properties, and on the basic of which proposes the judging algorithms of the specific evolution intentions.