高级检索

    软件构架动态行为建模与检测

    Modeling and Checking the Behavior of Software Architecture

    • 摘要: 针对软件构架描述语言在分析、验证软件构架动态行为中的不足,用抽象代数对构件、连接器和体系结构配置进行抽象,提出了软件构架层次模型,并采用Pr/T网对软件构架动态行为建模.提出基于线性时序逻辑的软件构架动态行为模型检测方法,给出了该方法的算法描述.最后,详细描述了电子商务系统中并发控制机制的建模过程和检测结果.提出的软件构架动态行为建模与检测方法结合了Pr/T网和线性时序逻辑的优点,为开展软件构架动态行为的分析、验证提供了理论基础.

       

      Abstract: 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.

       

    /

    返回文章
    返回