A Formalization Description Method for Software Architecture

摘要

In order to describe the dynamic property behavior of the software architecture precisely, this paper presents a unified framework of the software architecture based on LTL, constrains the elements of architecture and the connective relationship among the elements through the method of formalization description. The method proposed is verified by the example of TRIMCS, and the state behavior of system is deduced. So it provides theory foundation to analyze and validate the dynamic behavior of software architecture.