基于构图覆盖的软件需求检测方法

以需求描述模型RTRSM为基础，通过建立抽象的、能将控制流和数据流等有机地结合到一起的实时软件的动态执行模型，提出了构图覆盖的动态检测方法，并给出了其具体算法．该方法能检测嵌入式实时软件系统动态执行步中各并行成分及其相互间的执行情况，而且也可为分析员提供一些有用的检测信息以提高分析和检测软件需求的效率．     

基于整型区间集的数组越界静态自动测试方法研究

数组越界是软件中普遍存在的一种故障类型，并对软件安全造成了潜在的威胁．传统的故障检测使用程序插装的方法，并相应的以编译优化技术来排除掉多余的数组边界检查．这种检测方法不仅降低了程序运行效率，增加了开销，而且往往不能对故障进行彻底的测试，容易造成漏报．本文在对程序进行静态分析的基础上，通过引入区间概念，建立了整型区间集和数组区间集，进而给出了数组越界的故障模型，模型的建立对软件故障进行了规范．本文随后给出了故障检测算法，最后给出了实验．结果表明这种方法比以往的测试方法具有更强的故障检测能力．     

新型电子装备软件故障诊断方法研究

操作程序(软件)已成为新型电子装备的重要的组成部分．软件中存在的缺陷影响电子装备的战术与技术性能。为了检测和诊断电子装备操作软件故障．针对软件特点和故障特征．建立了软件故障诊断模型，分析了故障隔离方法，提出了基于故障报告信息的诊断策略。实践证明．该方法较好地解决了电子装备操作软件的故障诊断问题。     

基于锁集合的动态数据竞争检测方法

数据竞争使得共享存储程序难于调试．以前大部分针对共享存储程序的动态数据竞争检测工作都是通过维护发生序来实现．这种方法有一个重要缺点，即针对程序的一种输入，对程序的一次执行进行检测，不能检测出所有的可行数据竞争．文中利用存储一致性模型的框架模型，针对域一致性模型提出了增强发生序概念，并依此得出一种基于锁集合的动态数据竞争检测算法，克服了这个问题．在软件DSM系统JIAJIA上的实现获得了很好的性能，应用平均减速比为3．14．利用该方法，在TSP程序中找到了大量的读写数据竞争的情况．     

基于Verds的C语言子集的模型检测方法

针对现今软件使用逻辑错误的问题越来越多的出现,提出了对最流行最普遍的编程语言1语言子集的模型检测方法的研究．采用基于Verds工具的模型,运用C语言子集转化成Verds模型的算法,结合Verds工具和MAGIC工具实现模型检测．引入反例引导的抽象精化方法使模型检测解决状态爆炸的问题．     

软件模型检测中的抽象

软件模型检测对保证软件的正确性和可靠性具有十分重要的意义，而抽象是减轻模型检测中状态爆炸问题最重要的技术之一。本文综述当前广泛应用于软件模型检测中的抽象技术，介绍了该领域的进展及研究方向。     

一个基于响铃形故障检测率函数的软件可靠性增长模型

非齐次泊松过程类软件可靠性增长模型是评价软件产品可靠性指标的有效工具．影响软件可靠性增长模型评估和预测准确性的最重要的两个因素是软件中隐藏的初始故障数和故障检测率．一些非齐次泊松过程类模型假设故障检测率是不随测试时间变化的常量,有些模型假设故障检测率是增函数或减函数．这些假设或忽略了测试者的学习过程,或忽略了越迟被检测到的故障的概率就可能越低的特点．该文将测试者的学习过程和软件固有故障检测率的变化特征相结合,提出了一个铃形的故障检测率函数,建立了一个非齐次泊松过程类软件可靠性增长模型——Bbell—SRGM．在一组失效数据上的实验分析表明：对这组失效数据,Bbell—SRGM模型比G-O模型等的拟合效果更好．     

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

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

软件过程的JMOSP模型

由于软件过程模型在提高软件生产力方面具有重要的意义，它已经成为软件工程领域内的一个研究热点．本文在简单地分析了当前几种不同的软件过程模型的缺陷后，提出了软件过程的ＪＭＯＳＰ模型．     

基于CGOM的软件费用模型研究

软件测试是提高软件质量的重要手段，对测试数据充分的测试准则是软件测试完成的标准．目前，绝大多数的测试准则并不考虑软件费用，容易为了满足测试准则而使用户承担昂贵的测试费用．该文提出了一种随机过程类非齐次泊松过程(NHPP)中的经典模型——G-O模型的改进模型，并基于此模型构造了一个综合了软件设计费用、软件测试费用、软件维护费用、软件失效造成的风险损失的软件费用模型．最后从软件费用出发，讨论了软件的最佳发布时间．     

离散时段演算的符号模型验证

模型验证是对有限状态系统的一种形式化确认方法，近几年，模型验证方法已逐步扩展到实时系统应用中，为解决实时系统的模型验证问题，本文采用离散时段演算人实时系统规格说明的形式语言，用时间自动机作为实时系统的实现模型，对模型验证问题进行了细致的分析，并提出了一种具有实际应用价值的方法－商技术，该方法可以在避免当多个时间自动机并行组合时可能产生的状态空间组合爆炸问题，同时还可以简化整个模型验证问题。     

Model-checking games for fixpoint logics with partial order models

In this paper, we introduce model-checking games that allow local second-order power on sets of independent transitions in the underlying partial order models where the games are played. Since the interleaving semantics of such models is not considered, some problems that may arise when using interleaving representations are avoided and new decidability results for partial order models of concurrency are achieved. The games are shown to be sound and complete, and therefore determined. While in the interleaving case they coincide with the local model-checking games for the μ-calculus, in a partial order setting they verify properties of a number of fixpoint modal logics that can specify, in concurrent systems with partial order semantics, several properties not expressible with the μ-calculus. The games underpin a novel decision procedure for model-checking all temporal properties of a class of infinite and regular event structures, thus improving, in terms of temporal expressive power, previous results in the literature.     

Formal Verification of Websites

In this paper, a model for websites is presented. The model is well-suited for the formal verification of dynamic as well as static properties of the system. A website is defined as a collection of web pages which are semantically connected in some way. External web pages (which are related pages not belonging to the website) are treated as the environment of the system. We also present the logic which is used to specify properties of websites, and illustrate the kinds of properties that can be specified and verified by using a model-checking tool on the system. In this setting, we discuss some interesting properties which often need to be checked when designing websites. We have encoded the model using the specification language Maude which allows us to use the Maude model-checking tool.     

A Game Theoretic Approach to the Analysis of Dynamic Networks

A model of dynamic networks is introduced which incorporates three kinds of network changes: deletion of nodes (by faults or sabotage), restoration of nodes (by actions of “repair”), and creation of nodes (by actions that extend the network). The antagonism between the operations of deletion and restoration resp. creation is modelled by a game between the two agents “Destructor” and “Constructor”. In this framework of dynamic model-checking, we consider as specifications (“winning conditions” for Constructor) elementary requirements on connectivity of those networks which are reachable from some initial given network. We show some basic results on the (un-)decidability and hardness of dynamic model-checking problems.     

Model checking probabilistic systems against pushdown specifications

Model checking is a fully automatic verification technique traditionally used to verify finite-state systems against regular specifications. Although regular specifications have been proven to be feasible in practice, many desirable specifications are non-regular. For instance, requirements which involve counting cannot be formalized by regular specifications but using pushdown specifications, i.e., context-free properties represented by pushdown automata. Research on model-checking techniques for pushdown specifications is, however, rare and limited to the verification of non-probabilistic systems.In this paper, we address the probabilistic model-checking problem for systems modeled by discrete-time Markov chains and specifications that are provided by deterministic pushdown automata over infinite words. We first consider finite-state Markov chains and show that the quantitative and qualitative model-checking problem is solvable via a product construction and techniques that are known for the verification of probabilistic pushdown automata. Then, we consider recursive systems modeled by probabilistic pushdown automata with an infinite-state Markov chain semantics. We first show that imposing appropriate compatibility (visibility) restrictions on the synchronizations between the pushdown automaton for the system and the specification, decidability of the probabilistic model-checking problem can be established. Finally we prove that slightly departing from this compatibility assumption leads to the undecidability of the probabilistic model-checking problem, even for qualitative properties specified by deterministic context-free specifications.     

Refining Model Checking by Abstract Interpretation

Formal methods combining abstract interpretation and model-checking have been considered for automated analysis of software.In abstract model-checking, the semantics of an infinite transition system is abstracted to get a finite approximation on which temporal-logic/-calculus model-checking can be directly applied.The paper proposes two improvements of abstract model-checking which can be applied to infinite abstract transition systems:iA new combination of forwards and backwards abstract fixed-point model-checking computations for universal safety. It computes a more precise result than that computed by conjunction of the forward and backward analyses alone, without needing to refine the abstraction;When abstraction is unsound (as can happen in minimum/maximum path-length problems), it is proposed to use the partial results of a classical combination of forward and backward abstract interpretation analyses for universal safety in order to reduce, on-the-fly, the concrete state space to be searched by model-checking.     

Fixed-Point Logics and Solitaire Games

The model-checking games associated with fixed-point logics are parity games, and it is currently not known whether the strategy problem for parity games can be solved in polynomial time. We study Solitaire-LFP, a fragment of least fixed-point logic, whose evaluation games are nested soltaire games. This means that on each strongly connected component of the game, only one player can make nontrivial moves. Winning sets of nested solitaire games can be computed efficiently. The model-checking problem for Solitaire-LFP is Pspace-complete in general and Ptime-complete for formulae of bounded width. On finite structures (but not on infinite ones), Solitaire-LFP is equivalent to transitive closure logic. We also consider the solitaire fragment of guarded fixed-point logics. Due to the restricted quantification pattern of these logics, the associated games are small and therefore admit more efficient model-checking algorithms.     

Model checking rational agents

Agent-oriented programming techniques seem appropriate for developing systems that operate in complex, dynamic, and unpredictable environments. We aim to address this requirement by developing model-checking techniques for the (automatic or semiautomatic) verification of rational-agent systems written in a logic-based agent-oriented programming language. Typically, developers apply model-checking techniques to abstract models of a system rather than the system implementation. Although this is important for detecting design errors at an early stage, developers might still introduce errors during coding. In contrast, developers can directly apply our model-checking techniques to systems implemented in an agent-oriented programming language, automatically verifying agent systems without the usual gap between design and implementation. We developed our techniques for AgentSpeak, a rational-agent programming language based on the AgentSpeak (L) abstract agent-oriented programming language. AgentSpeak shares many features of the agent-oriented programming paradigm. Similarly, we've developed techniques for automatically translating AgentSpeak programs into the model specification language of existing model-checking systems. In this way, we reduce the problem of verifying that an AgentSpeak system has certain BDI logic properties to a conventional LTL model-checking problem.     

Combining partial order reductions with on-the-fly model-checking

Partial order model-checking is an approach to reduce time and memory in model-checking concurrent programs. On-the-fly model-checking is a technique to eliminate part of the search by intersecting an automaton representing the (negation of the) checked property with the state during its generation. We prove conditions under which these two methods can be combined in order to gain reduction from both. An extension of the model-checker SPIN, which implements this combination, is studied, showing substantial reduction over traditional search, not only in the number of reachable states, but directly in the amount of memory and time used. We also describe how to apply partial-order model-checking under given fairness assumptions.