期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

软件构架动态行为建模与检测 被引量：1

Modeling and Checking the Behavior of Software Architecture
在线阅读 下载PDF
导出
摘要 针对软件构架描述语言在分析、验证软件构架动态行为中的不足,用抽象代数对构件、连接器和体系结构配置进行抽象,提出了软件构架层次模型,并采用Pr/T网对软件构架动态行为建模·提出基于线性时序逻辑的软件构架动态行为模型检测方法,给出了该方法的算法描述·最后,详细描述了电子商务系统中并发控制机制的建模过程和检测结果·提出的软件构架动态行为建模与检测方法结合了Pr/T网和线性时序逻辑的优点,为开展软件构架动态行为的分析、验证提供了理论基础· 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 Ecommerce 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.
作者 何坚 覃征
机构地区 北京工业大学软件学院 西安交通大学电子与信息工程学院电子商务研究所
出处 《计算机研究与发展》 EI CSCD 北大核心 2005年第11期2018-2024,共7页 Journal of Computer Research and Development
基金 国家"八六三"高技术研究发展计划基金项目(2003AA412020) 陕西省"十五"科技发展计划基金项目(2000K08-G12)~~
关键词 软件构架 Pr/T网 线性时序逻辑 模型检测 software architecture Pr/T net linear temporal logic model checking
分类号 TP311.5 [自动化与计算机技术—计算机软件与理论]
  • 相关文献

参考文献12

  • 1Mary Shaw, David Garlan. Software architecture: Perspectives on an emerging discipline. http:∥www.cs. cmu. edu/afs/-cs. cmu.edu/project/vit/www/paper-abstracts/SoftArch. html, 1999-02-11/2003-08-25.
  • 2Robert J. Allen. A formal approach to software architecture:[Ph. D. dissertation]. Pittsburgh, PA: School of Computer Science Carnegie Mellon University, 1997.
  • 3Jeff Magee, Jeff Kramer. Dynamic structure in software architectures. The 4th ACM SIGSOFT Symposium on theFoundations of Software Engineering, San Fransisco, CA, 1996.
  • 4骆华俊,唐稚松,郑建丹.可视化体系结构描述语言XYZ/ADL[J].软件学报,2000,11(8):1024-1029. 被引量：29
  • 5R. Gerth, D. Peled, M. Vardi, et al. Simple on-the-fly automatic verification of linear temporal logic. The 15th Int'l Conf. Protocol Specification, Testing and Verification, Warsaw,Poland, 1996.
  • 6Nenad Medvidovic, Richard N. Taylor. A classification and comparison framework for software architecture description languages. IEEE Trans. Software Engineering, 2000, 26(1): 70～93.
  • 7He Jian, Fang Dingyi, Qin Zheng. A Formal approach to distributed software architecture. IEEE TENCOM' 02, Beijing,2002.
  • 8X. He. A formal definition of hierarchical predicate transition nets. In: Proc. 17th Int'l Conf. Application and Theory of Petri Nets, LNCS 1091. Berlin: Springer-Verlag, 1996. 212～229.
  • 9Jordi Cortadella, Michael Kishinevsky, Luciano Lavagno, et al.Deriving from finite transition system. IEEE Trans. Computers,1998, 47(8): 859～882.
  • 10Z. Manna, A. Pnueli. The Temporal Logic of Reactive and Concurrent System: Specification. Berlin: Spring-Verlag, 1992.

二级参考文献15

  • 1[1]A. Pnueli. The Temporal Semantics of Concurent Programs [J].Theoretical Computer Science, 1981, 13: 45-60.
  • 2[2]E.M. Clarke, et al. Automatic Verification of Finite State Concurrent System Using Temporal Logical Specification [J]. ACM transaction on Programming Language and Systems, 1986, 8(2): 244-263.
  • 3[3]Leslie Lamport. The Temporal Logic of Actions [J]. ACM transaction on Programming Language and Systems, 1994, 16(3): 872-923.
  • 4[4]E.M. Clarke, O. Grumberg, D. Peled. Model Checking. Cambridge[M], MA: MIT Press, 2001, 35-49.
  • 5[5]R. Gerth, D. Peled, M.Vardi, and P. Wolper. Simple On-the-fly Automatic Verification of Linear Temporal Logic [C]. In Proceedings of the 15th International Conference on Protocol Specification,Testing and Verification, Warsaw, Poland, 1993.
  • 6[6]Z. Manna, A. Pnueli. The Temporal Logic of Reactive and Concurrent System: Specification [M]. Spring-Verlag, 1992.
  • 7[7]A. Prasad Sistla, M. Y. Vardi and P. Wolper. The Complementation Problem for Btchi Automata with Applications to Temporal Logic [J].Theoretical Computer Science, 1987, 49: 217-237.
  • 8[8]C. Courcoubets, M. Vardi, P. Wolper and M. Yannakakis.Memory-Efficient Algorithms for the Verification of Temporal Properties [J]. Formal Methods in System Design, 1992, 1: 275-288.
  • 9[10]C. Girault, R. Valk. Petri Nets for System Engineering: A Guide to Modeling, Verification and Application [M]. Springer-Verlag, 2003.
  • 10[11]Jordi Cortadella and Michael. Deriving from Finite Transition System[J]. IEEE Transaction on Computers, 1998, 47(2).

共引文献35

同被引文献8

引证文献1

二级引证文献2

计算机研究与发展
2005年 第11期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部