软件行为运行时验证研究
|
摘要
随着软件系统在电信、金融等领域的广泛应用,软件系统规模越来越庞大,软件结构与软件行为日益复杂,人们对其正确性、可用性可靠性和安全性等可信性质提出了更高的要求和期望。论文分析了传统的软件质量保证方式,如：测试、验证以及运行时验证的特点。提出一种以软件运行行为为关注点的运行时验证与分析思想。
讨论了软件行为描述技术,设计了一种行为模式描述语言(BPDL),并给出了BPDL到确定状态自动机的自动转换方法。BPDL是一种简洁的、描述能力很强的语言,它可以对软件运行行为踪迹进行形式化描述,同时BPDL还可以用于描述软件行为规约。同以往描述语言不同,BPDL把软件之间复杂的交互行为看作是事件序列及行为约束,从而简化了交互行为描述的复杂性,便于对软件行为进行运行时验证和分析。
研究了软件运行时验证技术,提出了一个软件行为运行时验证框架。在该框架中对软件行为的验证分两个阶段进行。首先采用自动机原理验证单一事件序列是否符合行为规约,当违反行为规约的事件出现时,验证系统给出相应提示；然后,对与历史信息相关的复杂交互行为的验证则采用多实体贝叶斯网技术进行验证分析,通过交互实体运行期的实时经历和以往经历进行知识融合对交互实体的可信性进行实时地自动计算,对当前交互行为是否可信做出实时和客观地判断。该框架对交互行为的监测可灵活配置,验证分两个阶段进行既能有效减少对软件系统的性能影响,提高验证效率,又能保证验证分析的准确性。
实现了软件运行时行为验证原型系统,并在典型的应用环境中加以测试。详细阐述了原型系统中核心部件的实现,通过仿真测试和分析,验证和评价了论文提出的软件行为运行时验证机制的可行性和有效性。
With the wide application of software to telecommunication and finance, the scale of software systems is constantly expanding, and their structures and behaviors become more and more complicated. Therefore, people have more request and wish for their correctness, availability, reliability, safety, etc. Starting with an analysis of traditional quality controlling techniques like test and verification, and the features of runtime verification, this thesis presents the idea of runtime verification and analysis, with a focus on the pattern of software when it is running.
Firstly, this thesis designs a language for describing behavior patterns after discussing the technique of describing software behavior, and provides the method that BPDL can automatically shift to Deterministic Finite Automaton (DFA). BPDL is a simple language, capable of making a formal description of software behavior traces while software is running. Meanwhile, it can also describe regulations of software behavior. BPDL is different from traditional description languages in that it views the complicated interactive behaviors among softwares as a series of events and behavior regulations, thus simplifying interactive behavior description, and bringing more convenience to runtime verification and analysis of software behavior.
Secondly, based on a study of software runtime-verification techniques, this thesis presents a runtime verification framework, with a focus on software behavior. Within this framework, runtime verification is conducted at two levels. At the first level, the theory of DFA is adopted to check whether a single series of events conforms to behavior regulations or not. If behavior regulation violating occurs, the verification system gives some important attentions;Multi-Entity Bayesian Network(MEBN) technology is employed to verify and analyze complicated interactive behaviors, which are related to the past information. With the help of MEBN, the trustworthiness of on-going interactive entities can be automatically figured out, and then an immediate and objective judgment can be made, by combining real time experiences and past experiences of those entities. This framework allows flexible arrangement for interactive behavior monitoring. Verification and analysis can be conducted at two different levels, which can reduce software system performance influence, improve verification efficiency, and guarantee the correctness of verification and analysis.
Lastly, this thesis implements the mechanism for software behavior running verification, and testifies it a typical prototypical system. It illustrates how to implement the core components in typical prototypical system, and makes simulation tests to verify and assess feasibility and efficiency of the runtime verification system.
讨论了软件行为描述技术,设计了一种行为模式描述语言(BPDL),并给出了BPDL到确定状态自动机的自动转换方法。BPDL是一种简洁的、描述能力很强的语言,它可以对软件运行行为踪迹进行形式化描述,同时BPDL还可以用于描述软件行为规约。同以往描述语言不同,BPDL把软件之间复杂的交互行为看作是事件序列及行为约束,从而简化了交互行为描述的复杂性,便于对软件行为进行运行时验证和分析。
研究了软件运行时验证技术,提出了一个软件行为运行时验证框架。在该框架中对软件行为的验证分两个阶段进行。首先采用自动机原理验证单一事件序列是否符合行为规约,当违反行为规约的事件出现时,验证系统给出相应提示；然后,对与历史信息相关的复杂交互行为的验证则采用多实体贝叶斯网技术进行验证分析,通过交互实体运行期的实时经历和以往经历进行知识融合对交互实体的可信性进行实时地自动计算,对当前交互行为是否可信做出实时和客观地判断。该框架对交互行为的监测可灵活配置,验证分两个阶段进行既能有效减少对软件系统的性能影响,提高验证效率,又能保证验证分析的准确性。
实现了软件运行时行为验证原型系统,并在典型的应用环境中加以测试。详细阐述了原型系统中核心部件的实现,通过仿真测试和分析,验证和评价了论文提出的软件行为运行时验证机制的可行性和有效性。
With the wide application of software to telecommunication and finance, the scale of software systems is constantly expanding, and their structures and behaviors become more and more complicated. Therefore, people have more request and wish for their correctness, availability, reliability, safety, etc. Starting with an analysis of traditional quality controlling techniques like test and verification, and the features of runtime verification, this thesis presents the idea of runtime verification and analysis, with a focus on the pattern of software when it is running.
Firstly, this thesis designs a language for describing behavior patterns after discussing the technique of describing software behavior, and provides the method that BPDL can automatically shift to Deterministic Finite Automaton (DFA). BPDL is a simple language, capable of making a formal description of software behavior traces while software is running. Meanwhile, it can also describe regulations of software behavior. BPDL is different from traditional description languages in that it views the complicated interactive behaviors among softwares as a series of events and behavior regulations, thus simplifying interactive behavior description, and bringing more convenience to runtime verification and analysis of software behavior.
Secondly, based on a study of software runtime-verification techniques, this thesis presents a runtime verification framework, with a focus on software behavior. Within this framework, runtime verification is conducted at two levels. At the first level, the theory of DFA is adopted to check whether a single series of events conforms to behavior regulations or not. If behavior regulation violating occurs, the verification system gives some important attentions;Multi-Entity Bayesian Network(MEBN) technology is employed to verify and analyze complicated interactive behaviors, which are related to the past information. With the help of MEBN, the trustworthiness of on-going interactive entities can be automatically figured out, and then an immediate and objective judgment can be made, by combining real time experiences and past experiences of those entities. This framework allows flexible arrangement for interactive behavior monitoring. Verification and analysis can be conducted at two different levels, which can reduce software system performance influence, improve verification efficiency, and guarantee the correctness of verification and analysis.
Lastly, this thesis implements the mechanism for software behavior running verification, and testifies it a typical prototypical system. It illustrates how to implement the core components in typical prototypical system, and makes simulation tests to verify and assess feasibility and efficiency of the runtime verification system.
引文
[1]梅宏,王千祥,张路,等.软件分析技术进展[J].计算机学报,2009,32(9)：1697-1709.
[2].王怀民.构建协同共享的可信软件生产环境[J].中国计算机学会通讯.2009,5(2)：56-61.
[3].刘克,单志广,王戟,等.“可信软件基础研究”重大研究计划综述[J].中国科学基金,2008,3：145-151.
[4]. Trusted Computing Group. TCG Architecture Overview[R]. vl.2,282004,4.
[5].屈延文.软件行为学[M].北京：电子工业出版社.2004.
[6]. E.W.Dijkstra. http://www.cnsoft.cn/Exploiture/Softproject/Colligate/200112/7462_5.html.
[7]. K. Havelundl, G. Rosu. An Overview of the Runtime Verification Tool Java PathExplorer. Formal Methods in System Design.2004,24(2):189-215.
[8]. M. Kim, S. Kannan,I. Lee,O.Sokolsky. Java-MaC:a Run-time Assurance Tool for Java Programs[J]. Formal Methods in System Design.2004,24(2):129-155.
[9]. Feng Chen, Marcelo D'Amorim, and Grigore Rosu. Monitoring-Oriented Programming:A Tool-Supported Methodology for Higher Quality Object-Oriented Software[R]. Technical Report UIUCDCS-R-2004-2420, Univ. oflllinois Urbana.
[10].Zheng Li, Yan Jin, Jun Han. A Runtime Monitoring and Validation Framework for Web Service Interactions[C]. ASWEC'06.
[11].L Baresi, S Guinea. Towards Dynamic Monitoring of WS-BPEL Processes[C]. Proceedings of the 3rd International Conference on Service-Oriented Computing,2005.
[12].D. Kranzlmuller, S. Grabner, J. Volkert. Debugging with the MAD environment[J]. Parallel Computing,1997,23(1):199-217.
[13].Gu Q, Chen DX, Xie L. PSET:A validation system for object-oriented distributed programming language named NC++[J]. Journal of Software,1997,8(6):352-356.
[14].R. Hofman, K. Langendoen, H. Bal. Visualizing high_level communication and synchronization[C]. In:Narasimhan I, Lakshmi V, eds. Proceedings of the 2nd IEEE International Conference on Algorithms and Architectures for Parallel Processing (ICA3PP'96). Singapore:Institute of Electrical and Electronics Engineers, Inc.,1996. 37-43.
[15].GJ. Holzmann. The model checker SPIN[J]. IEEE Transactions on Software Engineering, 1997.,23(5):279-295.
[16].J. Magee, J. Kramer. Concurrency:State Models & Java Programs[M]. Indianapolis:Wiley, 1999.
[17].Y Liu, M Li, Q Wang,H Mei. Middleware based Runtime Monitoring and Analyzing Framework[J]. Chinese Journal of Electronics.2007,12A,:124-128.
[18].刘绍华魏峻黄涛.基于服务协作中间件的动态流程模型[J].软件学报.2004,15(10)：1431-1436.
[19].郭长国,朱俊,初宁.一种分布式软件运行时监控机制[J].计算机与数字工程.2008,36(11),：33-36.
[20].王友荣,曾庆凯.一种内嵌式程序行为监控框架IPBMF[J]计算机工程.2008,34(6),：82-84.
[21].万灿军,李长云.动态演化环境中可信软件行为监控研究与进展[J].计算机应用研究,2009,4(26)：1201-1204.
[22].G. Jerry, Y. Zhu, S. Shim. Monitoring Software Components and Component-Based Software[C]. Proceedings of the 24th IEEE Annual International Computer Software and Applications Conference, Taiwan,2000:403-412.
[23].P. Herrmann, H. Krumm. Trust-Adapted Enforcement of Security Policies in Distributed Component-Structured Applications[C]. Proceedings of the 6th IEEE Symposium on Computers and Communications, Hammamet, Tunesia,2001:2-8.
[24].K. Diakov, J. Batteram, H. Zandbel. Monitoring of Distributed Component Interactions[C]. Proceedings of the IFIP International Conference on Distributed Systems Platforms and Open Distributed Processing, New York,2000:229-243.
[25].P. Avgustinov, J. Tibble, E. Bodden, O. Lhotak. Aspect for Trace Monitoring. Formal Approaches to Testing Systems and Runtime Verification[C]. Seattle, WA, USA,2006: 20-39.
[26].F. Kon, M. Roman, P. Liu, J. Mao. Monitoring, Security, and Dynamic Configuration with the dynamicTAO Reflective ORB[C]. Proceedings of the IFIP International Conference on Distributed Systems Platforms and Open Distributed Processing (Middleware'2000), New York,2000,121-143.
[27].F. Chen, G. Rosu. MOP:An Efficient and Generic Runtime Verification Framework[C]. Proceedings of the 2007 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, Canada,2007:569-588.
[28].M. G. Uddin. Development and Automatic Monitoring of Trust-Aware Service-Based Software.Ph.D. Thesis, Canada:Queens University,2008.
[29].D. Garlan, S. W. Cheng, A. C. Huang. Rainbow:Architecture-based Self-Adaptation with Reusable Infrastructure[J]. IEEE Computer,2004,37(10):46-54.
[30].G. Rackl, M. Lindermeier, M. Rudorfer. B. Suss. MIMO-An Infrastructure for Monitoring and Managing Distributed Middleware Environments[C]. Middleware 2000, New York, 2000,71-87.
[31]. E. Bodden. A Lightweight LTL Runtime Verification Tool-for Java[C]. Proceedings of the 2004 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, Canada,2004:306-307.
[32].J. Li. Monitoring and Characterization of Component-Based Systems with Global Causality Capture[C]. Proceedings of the 23rd International Conference on Distributed Computing Systems, Rhode Island, USA,2003:422-431.
[33]. C.B.Jones. Systematic Software Development Using VDM [M]. Prentice Hall International (UK) Ltd. Hertfordshire, UK,1990:1-20.
[34].J.G. Hall, J.L. Jacob, J.A. McDermid, et al. Towards a Z Method:the Two Button Press Case Study [J]. IEEE Colloquium on Practical Application of Formal Methods,1995,19(5): 1-3.
[35],H. Habrias, B. Griech. Formal Specification of Dynamic Constraints with the B Method [C]. The 1st IEEE International Conference on Formal Engineering Methods. Hiroshima, Japan,1997:304-314.
[36].虞凡,覃征,贾晓琳等.基于XYZ/E规范的软件测试用例自动生成方法[J].计算机工程,2005,31(]9)：76-78.
[37].R. Barbuti, N. Francesco, A. Santone, et al. Reduced Models for Efficient CCS Verification [J]. Formal Methods in System Design,2005,26(3):319-350.
[38]. A. Mota, A. Sampaio. Model-checking CSP-Z [J]. Springer Lecture Notes in Computer Science,1998,1382:205-220.
[39].C. Bodei, P. Degano, F. Nielson, et al. Control Flow Analysis for the π-calculus [J]. Springer Lecture Notes in Computer Science.1998,1466:481-488
[40].P. H. Starke. Processes in Petri nets [J]. Springer Lecture Notes in Computer Science,1981, 117:350-359.
[41].金英,李泽鹏,张晶等.多线程Java程序安全行为模型的静态检查方法[J].计算机学报.2009,32(9)：1856-1868.
[42].蔡奎. Web界而中复杂行为建模及其代码自动生成[博士学位论文].济南 山东大学.2009.4.
[43].杨璐,柳溪,王林章,等.而向基于场景规约的Web服务消息流分析与验证[J]. 计算机学报,2009,32(9)：1759-1772.
[44]. R. S. Pressman. Software Engineering Software Engineering:A Practitioner's Approach(6th edition) [M]. McGraw-Hill, USA,2005:100-124.
[45].K. E. Wiegers, D. C. Sturzenberger. A Modular Software Process Mini-Assessment Method-Tool Report [J]. IEEE Software,2000,17(1):62-69.
[46].周颖,郑国梁,李宣东.而向模型检验的UML状态机语义[J].电子学报.2004,31(12)：2091-2095.
[47].K. J. Kristoffersen1, C. Pedersena, H. R. Andersena. Event-Based Runtime Checking of Timed LTL [J]. Electronic Notes in Theoretical Computer Science,2003,89(2):210-225
[48].N. Bouguila, J. H. Wang, A. B. Hamza. A Bayesian Approach for Software Quality Prediction[C]. The 4th International IEEE Conference on Intelligent Systems. Varna, Bulgaria,2008:49-54.
[49].R. Mello, L. Senger, L. Yang. Automatic text classification using an artificial neural network[J]. High Performance Computational Science and Engineering.2005,17(9):1-21.
[50].宋巍,马晓星, 吕建.Web服务组合动态演化的实例可迁移性[J].计算机学报.2009,32(9)：1816-1831.
[51]. S. Girish. Selection and Architecture-based Composition of Trust Models in Decentralized Applications[D]. P.hd Thesis. University of California, Irvine,2007:9-10.
[52].张岩,胡军,于笑丰,等.场景驱动的构件行为抽取[J].软件学报.2007 18(1)：50-61.
[53]. A. Bracciali, A. Brogi, C. Canal. A formal approach to component adaptation[J]. Journal of Systems and Software,2005,74(1):45-54.
[54].刘奕明,彭鑫,赵文耘,等.协作策略驱动的构件组合行为提取[C].2007全国软件及其应用学术会议论文集.
[55].IEEE Std 1012-2004 IEEE standard for software verificiation and validation.IEEE Std 1012-2004 (Revision of IEEE Std 1012-1998),2005,1-110.
[56].M.Leucker, C. Schallharta. A brief account of runtime verification[J].Journal of Logic and Algebraic Programming.2009,78(5):293-303.
[57].B.Meyer. Design by Contract, Components and Debugging[J]. In Journal of object-Oriented Programming.1999:75-79.
[58].A. Pnueli. The temporal logic of programs[C]. In Proceedings of the 18th IEEE Symposium on Foundations of Computer Science,1977:46-77.
[59]. W. S. McCullochl, W. Pitts. A logical calculus of the ideas immanent in nervous activity[J]. Bulletin of Mathematical Biology.1943,5(4):115-133.
[60].DM Ritchie, K Thompson. The UNIX time-sharing system[J]. Communications of the ACM.1983,26(5):84-89.
[61].王志兵,李长云.基于行为模式的电子交易过程中信任评估研究[J].计算机应用研究.2010,27(4)：945-947.
[62].万灿军.分布式软件的交互行为监测机制的设计与实现.[硕士学位论文].株洲 湖南工业大学.2009.
[63].J Man, X Wen, Z Wang and G Liu. Distributed Software Interactive Behavior Analysis. Based on Knowledge Fusion[C].2009 International Symposium on Information Processing. Huangshan,2009,8:441-444.
[64].K Thompson. Programming techniques:regular expression search algorithm[J]. Communications of the ACM,1968,11(6):419-422.
[65].赵常智,董威,隋平,等.面向参数化LTL的预测监控器构造技术[J].软件学报.2010,21(2)：318-333.
[66].Bauer A, Leucker M, Schallhart C. The good, the bad, and the ugly—But how ugly is ugly? In:Havelund K, Rosu G, eds. Proc. of the 7th Int'l Workshop on Runtime Verification. Vancouver:Springer-Verlag,2007.126-138.
[67].M. Kim,M. Viswanathan, H. Ben-Abdallah, S.Kannan, I. Lee, O. Sokolsky.MaC:A Framework for Run-time Correctness Assurance of Real-Time Systems[R]. MS-CIS-98-37, Department of Computer and Information Sciences, University of Pennsylvania.1998.
[68]. J Man, Z Wen, C Li, X Wen. Research on Running Time Behavior Analyzing and Trend Predicting of Modern Distributed Software[J]. Journal of Computers.2009,4(8):747-754.
[69].P. Costa. Bayesian Semantics for the Semantic Web [D]. PhD thesis, Department of Systems Engineering and Operational Research, George Mason University,2005:60-100.
[70].P. Costa,.Laskey K B. PR-OWL:A Framework for Probabilistic Ontologies [C]. The 4th International Conference on Formal Ontology in Information Systems, Baltimore, USA, 2006:30-41.
[71].K B. Laskey. MEBN:A Language for First-Order Bayesian Knowledge Bases [J]. Artificial Intelligence,2007,172(2-3):172-225.
[2].王怀民.构建协同共享的可信软件生产环境[J].中国计算机学会通讯.2009,5(2)：56-61.
[3].刘克,单志广,王戟,等.“可信软件基础研究”重大研究计划综述[J].中国科学基金,2008,3：145-151.
[4]. Trusted Computing Group. TCG Architecture Overview[R]. vl.2,282004,4.
[5].屈延文.软件行为学[M].北京：电子工业出版社.2004.
[6]. E.W.Dijkstra. http://www.cnsoft.cn/Exploiture/Softproject/Colligate/200112/7462_5.html.
[7]. K. Havelundl, G. Rosu. An Overview of the Runtime Verification Tool Java PathExplorer. Formal Methods in System Design.2004,24(2):189-215.
[8]. M. Kim, S. Kannan,I. Lee,O.Sokolsky. Java-MaC:a Run-time Assurance Tool for Java Programs[J]. Formal Methods in System Design.2004,24(2):129-155.
[9]. Feng Chen, Marcelo D'Amorim, and Grigore Rosu. Monitoring-Oriented Programming:A Tool-Supported Methodology for Higher Quality Object-Oriented Software[R]. Technical Report UIUCDCS-R-2004-2420, Univ. oflllinois Urbana.
[10].Zheng Li, Yan Jin, Jun Han. A Runtime Monitoring and Validation Framework for Web Service Interactions[C]. ASWEC'06.
[11].L Baresi, S Guinea. Towards Dynamic Monitoring of WS-BPEL Processes[C]. Proceedings of the 3rd International Conference on Service-Oriented Computing,2005.
[12].D. Kranzlmuller, S. Grabner, J. Volkert. Debugging with the MAD environment[J]. Parallel Computing,1997,23(1):199-217.
[13].Gu Q, Chen DX, Xie L. PSET:A validation system for object-oriented distributed programming language named NC++[J]. Journal of Software,1997,8(6):352-356.
[14].R. Hofman, K. Langendoen, H. Bal. Visualizing high_level communication and synchronization[C]. In:Narasimhan I, Lakshmi V, eds. Proceedings of the 2nd IEEE International Conference on Algorithms and Architectures for Parallel Processing (ICA3PP'96). Singapore:Institute of Electrical and Electronics Engineers, Inc.,1996. 37-43.
[15].GJ. Holzmann. The model checker SPIN[J]. IEEE Transactions on Software Engineering, 1997.,23(5):279-295.
[16].J. Magee, J. Kramer. Concurrency:State Models & Java Programs[M]. Indianapolis:Wiley, 1999.
[17].Y Liu, M Li, Q Wang,H Mei. Middleware based Runtime Monitoring and Analyzing Framework[J]. Chinese Journal of Electronics.2007,12A,:124-128.
[18].刘绍华魏峻黄涛.基于服务协作中间件的动态流程模型[J].软件学报.2004,15(10)：1431-1436.
[19].郭长国,朱俊,初宁.一种分布式软件运行时监控机制[J].计算机与数字工程.2008,36(11),：33-36.
[20].王友荣,曾庆凯.一种内嵌式程序行为监控框架IPBMF[J]计算机工程.2008,34(6),：82-84.
[21].万灿军,李长云.动态演化环境中可信软件行为监控研究与进展[J].计算机应用研究,2009,4(26)：1201-1204.
[22].G. Jerry, Y. Zhu, S. Shim. Monitoring Software Components and Component-Based Software[C]. Proceedings of the 24th IEEE Annual International Computer Software and Applications Conference, Taiwan,2000:403-412.
[23].P. Herrmann, H. Krumm. Trust-Adapted Enforcement of Security Policies in Distributed Component-Structured Applications[C]. Proceedings of the 6th IEEE Symposium on Computers and Communications, Hammamet, Tunesia,2001:2-8.
[24].K. Diakov, J. Batteram, H. Zandbel. Monitoring of Distributed Component Interactions[C]. Proceedings of the IFIP International Conference on Distributed Systems Platforms and Open Distributed Processing, New York,2000:229-243.
[25].P. Avgustinov, J. Tibble, E. Bodden, O. Lhotak. Aspect for Trace Monitoring. Formal Approaches to Testing Systems and Runtime Verification[C]. Seattle, WA, USA,2006: 20-39.
[26].F. Kon, M. Roman, P. Liu, J. Mao. Monitoring, Security, and Dynamic Configuration with the dynamicTAO Reflective ORB[C]. Proceedings of the IFIP International Conference on Distributed Systems Platforms and Open Distributed Processing (Middleware'2000), New York,2000,121-143.
[27].F. Chen, G. Rosu. MOP:An Efficient and Generic Runtime Verification Framework[C]. Proceedings of the 2007 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, Canada,2007:569-588.
[28].M. G. Uddin. Development and Automatic Monitoring of Trust-Aware Service-Based Software.Ph.D. Thesis, Canada:Queens University,2008.
[29].D. Garlan, S. W. Cheng, A. C. Huang. Rainbow:Architecture-based Self-Adaptation with Reusable Infrastructure[J]. IEEE Computer,2004,37(10):46-54.
[30].G. Rackl, M. Lindermeier, M. Rudorfer. B. Suss. MIMO-An Infrastructure for Monitoring and Managing Distributed Middleware Environments[C]. Middleware 2000, New York, 2000,71-87.
[31]. E. Bodden. A Lightweight LTL Runtime Verification Tool-for Java[C]. Proceedings of the 2004 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, Canada,2004:306-307.
[32].J. Li. Monitoring and Characterization of Component-Based Systems with Global Causality Capture[C]. Proceedings of the 23rd International Conference on Distributed Computing Systems, Rhode Island, USA,2003:422-431.
[33]. C.B.Jones. Systematic Software Development Using VDM [M]. Prentice Hall International (UK) Ltd. Hertfordshire, UK,1990:1-20.
[34].J.G. Hall, J.L. Jacob, J.A. McDermid, et al. Towards a Z Method:the Two Button Press Case Study [J]. IEEE Colloquium on Practical Application of Formal Methods,1995,19(5): 1-3.
[35],H. Habrias, B. Griech. Formal Specification of Dynamic Constraints with the B Method [C]. The 1st IEEE International Conference on Formal Engineering Methods. Hiroshima, Japan,1997:304-314.
[36].虞凡,覃征,贾晓琳等.基于XYZ/E规范的软件测试用例自动生成方法[J].计算机工程,2005,31(]9)：76-78.
[37].R. Barbuti, N. Francesco, A. Santone, et al. Reduced Models for Efficient CCS Verification [J]. Formal Methods in System Design,2005,26(3):319-350.
[38]. A. Mota, A. Sampaio. Model-checking CSP-Z [J]. Springer Lecture Notes in Computer Science,1998,1382:205-220.
[39].C. Bodei, P. Degano, F. Nielson, et al. Control Flow Analysis for the π-calculus [J]. Springer Lecture Notes in Computer Science.1998,1466:481-488
[40].P. H. Starke. Processes in Petri nets [J]. Springer Lecture Notes in Computer Science,1981, 117:350-359.
[41].金英,李泽鹏,张晶等.多线程Java程序安全行为模型的静态检查方法[J].计算机学报.2009,32(9)：1856-1868.
[42].蔡奎. Web界而中复杂行为建模及其代码自动生成[博士学位论文].济南 山东大学.2009.4.
[43].杨璐,柳溪,王林章,等.而向基于场景规约的Web服务消息流分析与验证[J]. 计算机学报,2009,32(9)：1759-1772.
[44]. R. S. Pressman. Software Engineering Software Engineering:A Practitioner's Approach(6th edition) [M]. McGraw-Hill, USA,2005:100-124.
[45].K. E. Wiegers, D. C. Sturzenberger. A Modular Software Process Mini-Assessment Method-Tool Report [J]. IEEE Software,2000,17(1):62-69.
[46].周颖,郑国梁,李宣东.而向模型检验的UML状态机语义[J].电子学报.2004,31(12)：2091-2095.
[47].K. J. Kristoffersen1, C. Pedersena, H. R. Andersena. Event-Based Runtime Checking of Timed LTL [J]. Electronic Notes in Theoretical Computer Science,2003,89(2):210-225
[48].N. Bouguila, J. H. Wang, A. B. Hamza. A Bayesian Approach for Software Quality Prediction[C]. The 4th International IEEE Conference on Intelligent Systems. Varna, Bulgaria,2008:49-54.
[49].R. Mello, L. Senger, L. Yang. Automatic text classification using an artificial neural network[J]. High Performance Computational Science and Engineering.2005,17(9):1-21.
[50].宋巍,马晓星, 吕建.Web服务组合动态演化的实例可迁移性[J].计算机学报.2009,32(9)：1816-1831.
[51]. S. Girish. Selection and Architecture-based Composition of Trust Models in Decentralized Applications[D]. P.hd Thesis. University of California, Irvine,2007:9-10.
[52].张岩,胡军,于笑丰,等.场景驱动的构件行为抽取[J].软件学报.2007 18(1)：50-61.
[53]. A. Bracciali, A. Brogi, C. Canal. A formal approach to component adaptation[J]. Journal of Systems and Software,2005,74(1):45-54.
[54].刘奕明,彭鑫,赵文耘,等.协作策略驱动的构件组合行为提取[C].2007全国软件及其应用学术会议论文集.
[55].IEEE Std 1012-2004 IEEE standard for software verificiation and validation.IEEE Std 1012-2004 (Revision of IEEE Std 1012-1998),2005,1-110.
[56].M.Leucker, C. Schallharta. A brief account of runtime verification[J].Journal of Logic and Algebraic Programming.2009,78(5):293-303.
[57].B.Meyer. Design by Contract, Components and Debugging[J]. In Journal of object-Oriented Programming.1999:75-79.
[58].A. Pnueli. The temporal logic of programs[C]. In Proceedings of the 18th IEEE Symposium on Foundations of Computer Science,1977:46-77.
[59]. W. S. McCullochl, W. Pitts. A logical calculus of the ideas immanent in nervous activity[J]. Bulletin of Mathematical Biology.1943,5(4):115-133.
[60].DM Ritchie, K Thompson. The UNIX time-sharing system[J]. Communications of the ACM.1983,26(5):84-89.
[61].王志兵,李长云.基于行为模式的电子交易过程中信任评估研究[J].计算机应用研究.2010,27(4)：945-947.
[62].万灿军.分布式软件的交互行为监测机制的设计与实现.[硕士学位论文].株洲 湖南工业大学.2009.
[63].J Man, X Wen, Z Wang and G Liu. Distributed Software Interactive Behavior Analysis. Based on Knowledge Fusion[C].2009 International Symposium on Information Processing. Huangshan,2009,8:441-444.
[64].K Thompson. Programming techniques:regular expression search algorithm[J]. Communications of the ACM,1968,11(6):419-422.
[65].赵常智,董威,隋平,等.面向参数化LTL的预测监控器构造技术[J].软件学报.2010,21(2)：318-333.
[66].Bauer A, Leucker M, Schallhart C. The good, the bad, and the ugly—But how ugly is ugly? In:Havelund K, Rosu G, eds. Proc. of the 7th Int'l Workshop on Runtime Verification. Vancouver:Springer-Verlag,2007.126-138.
[67].M. Kim,M. Viswanathan, H. Ben-Abdallah, S.Kannan, I. Lee, O. Sokolsky.MaC:A Framework for Run-time Correctness Assurance of Real-Time Systems[R]. MS-CIS-98-37, Department of Computer and Information Sciences, University of Pennsylvania.1998.
[68]. J Man, Z Wen, C Li, X Wen. Research on Running Time Behavior Analyzing and Trend Predicting of Modern Distributed Software[J]. Journal of Computers.2009,4(8):747-754.
[69].P. Costa. Bayesian Semantics for the Semantic Web [D]. PhD thesis, Department of Systems Engineering and Operational Research, George Mason University,2005:60-100.
[70].P. Costa,.Laskey K B. PR-OWL:A Framework for Probabilistic Ontologies [C]. The 4th International Conference on Formal Ontology in Information Systems, Baltimore, USA, 2006:30-41.
[71].K B. Laskey. MEBN:A Language for First-Order Bayesian Knowledge Bases [J]. Artificial Intelligence,2007,172(2-3):172-225.