【作者】 王志兵；

【导师】 李长云；

【作者基本信息】 湖南工业大学 ， 计算机软件与理论， 2010， 硕士

【摘要】 随着软件系统在电信、金融等领域的广泛应用,软件系统规模越来越庞大,软件结构与软件行为日益复杂,人们对其正确性、可用性可靠性和安全性等可信性质提出了更高的要求和期望。论文分析了传统的软件质量保证方式,如：测试、验证以及运行时验证的特点。提出一种以软件运行行为为关注点的运行时验证与分析思想。讨论了软件行为描述技术,设计了一种行为模式描述语言(BPDL),并给出了BPDL到确定状态自动机的自动转换方法。BPDL是一种简洁的、描述能力很强的语言,它可以对软件运行行为踪迹进行形式化描述,同时BPDL还可以用于描述软件行为规约。同以往描述语言不同,BPDL把软件之间复杂的交互行为看作是事件序列及行为约束,从而简化了交互行为描述的复杂性,便于对软件行为进行运行时验证和分析。研究了软件运行时验证技术,提出了一个软件行为运行时验证框架。在该框架中对软件行为的验证分两个阶段进行。首先采用自动机原理验证单一事件序列是否符合行为规约,当违反行为规约的事件出现时,验证系统给出相应提示；然后,对与历史信息相关的复杂交互行为的验证则采用多实体贝叶斯网技术进行验证分析,通过交互实体运行期的实时经历和以往经历进行知识融合对交互实体的可信性进行实时地自动计算,对当前交互行为是否可信做出实时和客观地判断。该框架对交互行为的监测可灵活配置,验证分两个阶段进行既能有效减少对软件系统的性能影响,提高验证效率,又能保证验证分析的准确性。实现了软件运行时行为验证原型系统,并在典型的应用环境中加以测试。详细阐述了原型系统中核心部件的实现,通过仿真测试和分析,验证和评价了论文提出的软件行为运行时验证机制的可行性和有效性。更多还原

【Abstract】 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.更多还原