Since　architecture　description　languages　are　not　capable　enough　in　analyzing　and　validating　the　dynamic　behavior　of　software　architecture,　the　hierarchical　framework　for　software　architecture　is　proposed　in　this　paper,　in　which　the　abstract　algebra　is　used　to　abstract　the　components,　connectors　and　architectural　configuration.　Meanwhile,　the　predicate　transition　(Pr/T)　net　is　introduced　to　model　the　dynamic　behavior　of　software　architecture,　and　an　efficient　model-checking　algorithm　based　on　the　linear　temporal　logic　(LTL)　is　discussed　in　details.　Finally,　the　approach　to　model　a　current　control　mechanism　in　an　E-commerce　system　and　checking　results　based　on　LTL　are　shown　in　details.　It　can　be　demonstrated　by　practice　that　the　modeling-and-checking　method　presented　combines　the　advantages　of　linear　temporal　logic　with　those　of　Pr/T　net,　so　that　it　provides　novel　approaches　to　analyze　and　validate　the　dynamic　behavior　of　software　architecture.