分布式软件系统交互行为建模、验证与测试

为了确保分析与设计阶段分布式软件系统中模块之间交互行为的正确性,提出了一种分布式软件系统模块交互的抽象方法,分别通过系统状态机图和对象状态机图对各模块状态变迁进行建模,使用UML2．0序列图对模块之间交互行为进行描述．采用基于命题投影时序逻辑的模型检测技术,将对象状态机图转换为 Promela 模型,系统交互性质转换为命题投影时序逻辑公式,通过模型检测器验证交互模型是否满足于系统的性质,若不满足于该性质,则能够获得反例执行的路径．给出了一个分布式软件系统测试框架,在验证后的序列图模型基础上,使用基于模型的测试用例自动生成方法得到测试用例集合,该集合能够实现对交互行为的有效测试．实例结果表明,该方法可以提高分布式软件系统中模块交互行为的有效性和可靠性．     

基于反例确认的CPS不确定性模型校准

信息物理系统被广泛应用于众多关键领域,例如工业控制与智能制造.作为部署在这些关键领域中的系统,其系统质量尤为重要.然而,由于信息物理系统自身的复杂性以及系统中存在的不确定性（例如系统通过传感器感知环境时的偏差）,信息物理系统的质量保障面临巨大挑战.验证是保障系统质量的有效途径之一,基于系统模型与规约它可以证明系统是否满足要求的性质.现有一些信息物理系统的验证工作也取得了显著进展,例如模型检验技术就被已用工作用于验证系统在不确定性影响下的行为是否满足性质规约,并在性质违反的情况给出具体的反例.这些验证工作的一个重要输入就是不确定性模型,它描述了系统中不确定性的具体情况.而实际中要对系统中不确定性精确建模却并非易事,因此验证中使用的不确定性模型很可能与实际不完全相符,这将导致验证结果不准确并与现实偏离.针对这一问题,本文提出了一种基于反例确认的不确定性模型校准方法,来进一步精化验证结果以提高其准确度.首先通过确认反例在系统的执行中能否被触发来判断验证使用的不确定性模型是否精确.对于不精确的模型再利用遗传算法进行校准,并根据反例确认的结果来构造遗传算法的适应度函数以指导搜索,最后结合假设检验来帮助决定是否接受校准后的结果.在代表案例上的实验结果表明了我们提出的不确定性模型校准方法的有效性.     

三值逻辑证明系统及正例与反例的提取

三值逻辑模型检验是对更高层的模型抽象验证的一种方法,对其验证中常常需要给出正例和反例.为此,讨论了三值逻辑模型检验以及正例和反例的提取,并在给出一套三值逻辑证明规则的基础上形成一个证明系统;运用该系统可以证明模型是否满足某个性质;在证明过程中为存在路径量词提取正例,为全称路径量词提取反例.正例和反例的提取可给模型的细化指明方向.最后通过实例给出了该证明系统在数字逻辑电路验证中的应用.     

面向复杂随机系统的启发式统计模型检测方法 *

统计模型检测是一种高效的验证技术,常用于复杂的随机系统验证,如分布式算法等。而在超长路径上对性质进行验证时,其验证效率会急剧降低。为解决这个问题,这里提出一种启发式的统计模型检测算法。在对路径进行验证时,我们会查找帮助剪枝的最短前缀。并在后续抽样时,利用前缀信息直接判定路径是否满足给定性质,避免进入费时的路径验证阶段。在与PRISM的比较中,它的路径验证次数相对更少且平均抽样路径长度更短。因此使统计模型检测技术可应用于超长路径上的性质验证。     

基于ASP的CSP模型验证性质反例生成技术研究

为了解决当前通信顺序进程(CSP)模型检测不支持在验证工具的一次运行中验证多个性质的问题,建立了基于ASP的CSP并发模型验证框架。主要研究在该框架下当待验证的系统性质不满足时生成相应性质反例的技术。把ASP程序调试中的ASP程序支撑原因分析技术应用于该问题的研究,提出了相应的反例生成算法,实例表明了该算法的正确性。     

一种基于抽象与精化技术的Web服务组合验证方法

模型检测因其自动化程度高、能够提供反例路径等优势,被广泛应用于Web服务组合的兼容性验证。本文针对模型检测过程中存在的状态爆炸问题,在传统的模型检测方法中引入谓词抽象和精化技术,提出了一种针对Web服务组合的抽象精化验证框架。使用谓词抽象技术对原子Web服务抽象建模,将各Web服务抽象模型组合成组合抽象模型;将模型检测后得到的反例在各原子Web服务上做投影操作,对投影反例进行确认;对产生伪反例的Web服务抽象模型进行精化,生成新的组合抽象模型,再次对性质进行验证。最后通过实例分析说明基于抽象精化技术的Web服务组合验证框架在缓解状态爆炸问题上的可行性。     

基于关键迹和ASP的CSP模型检测

模型检测是通信顺序进程(communicating sequential processes,简称CSP)形式化验证的重要手段.当前, CSP模型检测方法基于操作语义,需将进程转化为迁移系统,进而提取语义模型,但转化过程较为复杂;待验证性质采用CSP语言进行描述,虽然有利于精炼检测(refinement checking),但描述能力较弱,通用性不强.鉴于此,提出了一种新的CSP指称语义模型——关键迹模型(critical-trace model)及基于该指称语义模型的CSP模型检测方法,并证明了其验证的可靠性,避免了上述问题.关键迹模型采用递归策略计算,待验证性质采用线性时态逻辑(linear temporal logic,简称LTL)描述.基于回答集程序设计(answer set programming,简称ASP)实现了关键迹模型的自动生成及LTL的自动验证,并开发了一个CSP模型检测原型系统——T_ASP.实验结果表明:与类似系统相比,该系统的描述能力更强,验证结果的准确性更高,且可同时验证多条性质,在性质不满足时还可提供多条反例.     

模型检测基于概率时间自动机的反例产生研究

模型检测基于概率系统的反例产生问题,在最近引起人们的关注.已有的工作主要围绕模型检测Markov链的反例产生而开展.基于概率时间自动机(PTA)是Markov链的不确定性和系统时钟的扩展.关注的是模型检测PTA的反例产生问题.首先通过在PTA上寻找概率之和恰好大于λ的κ条最大概率的路径,并根据这些路径和原PTA构造原PTA的一个子图,从而快速找到违背性质的具有较少证据的反例.然后精化此结果——通过逐条加入上述各条最大概率的路径来精确地计算已加入路径所构成的PTA子图的最大概率.由于考虑到符号状态交集对概率系统的影响,可以得到证据更少的反例.     

安全协议的扩展Horn逻辑模型及其验证方法

分析了Bruno Blanchet和Martin Abadi提出的基于Horn逻辑的安全协议模型及其验证方法，针对它们构造不满足安全性质的安全协议反例的不足，提出了安全协议的扩展Horn逻辑模型和修改版本的安全协议验证方法，使得能够从安全协议的扩展Horn逻辑模型和修改版本的安全协议验证过程中自动构造不满足安全性质的安全协议反例．在基于函数式编程语言Objective Carol开发的安全协议验证工具SPVT中，实现了上述算法，验证了算法的正确性．     

模型精化过程中模型间一致性检测研究

传统的模型精化过程中模型间一致性检测专注于检测模型自身的正确性、死锁、以及不变式保持性等,而无法保证模型间行为方面的一致性。为此提出利用系统行为属性来反应模型行为,结合模型检测的方法来检测模型间的行为一致性。首先对精化前模型分析生成抽象测试用例并抽取其代表的系统行为属性;然后根据精化后的模型抽取模型精化关系并进一步更新系统属性;最后使用这些系统行为属性来验证精化后的模型是否依然满足其代表的系统行为,如果不满足则说明模型间存在不一致行为,可以通过生成的反例路径找出不一致的位置。实验结果表明使用该方法可以有效找出模型精化前后的大多数不一致行为。     

Abstraction for model checking multi-agent systems

Model checking multi-agent systems (MAS) always suffers from the state explosion problem. In this paper we focus on an abstraction technique which is one of the major methods for overcoming this problem. For a multi-agent system, we present a novel abstraction procedure which reduces the state space by collapsing the global states in the system. The abstraction is automatically computed according to the property to be verified. The resulting abstract system simulates the concrete system, while the universal temporal epistemic properties are preserved. Our abstraction is an overapproximation. If some universal temporal epistemic property is not satisfied, then we need to identify spurious counterexamples. We further show how to reduce complex counterexamples to simple structures, i.e., paths and loops, such that the counterexamples can be checked and the abstraction can be refined efficiently. Finally, we illustrate the abstraction technique with a card game.     

Generating counterexamples for quantitative safety specifications in probabilistic B

Probabilistic annotations generalise standard Hoare Logic [20] to quantitative properties of probabilistic programs. They can be used to express critical expected values over program variables that must be maintained during program execution. As for standard program development, probabilistic assertions can be checked mechanically relative to an appropriate program semantics. In the case that a mechanical prover is unable to complete such validity checks then a counterexample to show that the annotation is incorrect can provide useful diagnostic information. In this paper, we provide a definition of counterexamples as failure traces for probabilistic assertions within the context of the pB language [19], an extension of the standard B method [1] to cope with probabilistic programs. In addition, we propose algorithmic techniques to find counterexamples where they exist, and suggest a ranking mechanism to return ‘the most useful diagnostic information’ to the pB developer to aid the resolution of the problem.     

Fate and free will in error traces

The ability to generate counterexamples for failing properties is often cited as one of the strengths of model checking. However, it is often difficult to interpret long error traces in which many variables appear. Besides, a traditional error trace presents only one possible behavior of the system causing the failure, with no further annotation. Our objective is to identify some structure in the error trace to make debugging easier. We present an enhanced error trace as an alternation of fated (forced) and free segments. The fated segments show unavoidable progress toward the error while the free segments show choices that, if avoided, may have prevented the error. Hence, the demarcation into segments tends to highlight critical events. The segmentation of a trace raises the questions of whether the fated segment should indeed be inevitable and whether the free segments are critical in causing the error. Addressing these questions may help the user to better analyze the failure of the property.     

Directed Explicit State-Space Search in the Generation of Counterexamples for Stochastic Model Checking

Current stochastic model checkers do not make counterexamples for property violations readily available. In this paper, we apply directed explicit state-space search to discrete and continuous-time Markov chains in order to compute counterexamples for the violation of PCTL or CSL properties. Directed explicit state-space search algorithms explore the state space on-the-fly, which makes our method very efficient and highly scalable. They can also be guided using heuristics which usually improve the performance of the method. Counterexamples provided by our method have two important properties. First, they include those traces which contribute the greatest amount of probability to the property violation. Hence, they show the most probable offending execution scenarios of the system. Second, the obtained counterexamples tend to be small. Hence, they can be effectively analyzed by a human user. Both properties make the counterexamples obtained by our method very useful for debugging purposes. We implemented our method based on the stochastic model checker PRISM and applied it to a number of case studies in order to illustrate its applicability.     

Run-Time Checking of Dynamic Properties

We consider a first-order property specification language for run-time monitoring of dynamic systems. The language is based on a linear-time temporal logic and offers two kinds of quantifiers to bind free variables in a formula. One kind contains the usual first-order quantifiers that provide for replication of properties for dynamically created and destroyed objects in the system. The other kind, called attribute quantifiers, is used to check dynamically changing values within the same object. We show that expressions in this language can be efficiently checked over an execution trace of a system.     

Iterative learning from positive data and negative counterexamples

A model for learning in the limit is defined where a (so-called iterative) learner gets all positive examples from the target language, tests every new conjecture with a teacher (oracle) if it is a subset of the target language (and if it is not, then it receives a negative counterexample), and uses only limited long-term memory (incorporated in conjectures). Three variants of this model are compared: when a learner receives least negative counterexamples, the ones whose size is bounded by the maximum size of input seen so far, and arbitrary ones. A surprising result is that sometimes absence of bounded counterexamples can help an iterative learner whereas arbitrary counterexamples are useless. We also compare our learnability model with other relevant models of learnability in the limit, study how our model works for indexed classes of recursive languages, and show that learners in our model can work in non-U-shaped way—never abandoning the first right conjecture.     

Verification of Safety Properties Using Integer Programming: Beyond the State Equation

The state equation is a verification technique that has been applied—not always under this name—to numerous systems modelled as Petri nets or communicating automata. Given a safety property P, the state equation is used to derive a necessary condition for P to hold which can be mechanically checked. The necessary conditions derived from the state equation are known to be of little use for systems communicating by means of shared variables, in the sense that many of these systems satisfy the property but not the conditions. In this paper, we use traps, a well-known notion of net theory, to obtain stronger conditions that can still be efficiently checked. We show that the new conditions significantly extend the range of verifiable systems.     

A framework for counterexample generation and exploration

Model-checking is becoming an accepted technique for debugging hardware and software systems. Debugging is based on the “Check/Analyze/Fix” loop: check the system against a desired property, producing a counterexample when the property fails to hold; analyze the generated counterexample to locate the source of the error; fix the flawed artifact—the property or the model. The success of model-checking non-trivial systems critically depends on making this Check/Analyze/Fix loop as tight as possible. In this paper, we concentrate on the Analyze part of the debugging loop. To this end, we present a framework for generating, structuring and exploring counterexamples, implemented in a tool called KEGVis. The framework is based on the idea that the most general type of evidence to why a property holds or fails to hold is a proof. Such proofs can be presented to the user in the form of proof-like counterexamples, without sacrificing any of the intuitiveness and close relation to the model that users have learned to expect from model-checkers. Moreover, proof generation is flexible, and can be controlled by strategies, whether built into the tool or specified by the user, thus enabling generation of the most “interesting” counterexample and its interactive exploration. Moreover, proofs can be used to generate and display all relevant evidence together, a technique referred to as abstract counterexamples. Overall, our framework can be used for explaining the reason why the property failed or succeeded, determining whether the property was correct (“specification debugging”), and for general model exploration.     

使用事件自动机规约的C语言有界模型检测

提出使用事件自动机对 C 程序的安全属性进行规约,并给出了基于有界模型检测的形式化验证方法。事件自动机可以规约程序中基于事件的安全属性,且可以描述无限状态的安全属性。事件自动机将属性规约与C程序本身隔离,不会改变程序的结构。在事件自动机的基础上,提出了自动机可达树的概念。结合自动机可达树和有界模型检测技术,给出将事件自动机和C程序转化为可满足性模理论SMT(satisfiability modulo theory)模型的算法。最后,使用SMT求解器对生成的SMT模型求解,并根据求解结果给出反例路径分析算法。实例分析和实验结果表明,该方法可以有效验证软件系统中针对事件的属性规约。     

基于Assume-Guarantee搜索复用的C程序验证方法

提出了一种基于Assume-Guarantee搜索复用的验证方法,对C程序源代码进行验证.其思想是,在程序的每点处都引入一个保守假设条件,并假设从任意点出发,变量取值满足该点假设条件的所有执行路径都不会违背给定性质,然后根据这些假设条件遍历所有可能的执行路径以验证给定的时序安全性质,并在遍历的过程中验证这些假设条件是否满足,如果不满足,则不断对其精化和加强.验证方法总是在保证假设条件可靠的前提下尽量使用较弱的条件,使得大量的执行路径由于满足假设条件而可以搜索复用,从而降低验证代价.应用该方法验证了Linux操作系统中SSL协议的实现程序openssl-0.9.6c满足SSL协议的初始握手规范.实验结果表明,该方法具有良好的实用性和可扩展性.