一种面向CPS的自适应统计模型检测方法

随着计算机与物理环境的交互日益密切,信息物理融合系统（cyber physical systems,CPSs）在健康医疗、航空电子、智能建筑等领域有着广泛的应用前景,CPSs的正确性、可靠性分析已引起人们的广泛关注.统计模型检测（statistical model checking,SMC）技术能够对CPSs进行有效验证,并为系统的性能提供定量评估.然而,随着系统规模的日益扩大,如何提高统计模型检测技术验证CPSs的效率,是目前所面临的主要困难之一.针对此问题,本文首先对现有SMC技术进行实验分析,总结各种SMC技术的受限适用范围和性能缺陷,并针对贝叶斯区间估计算法（Bayesian Interval Estimate,BIE）在实际概率接近0.5时需要大量路径才能完成验证的缺陷,提出一种基于抽象和学习的统计模型检测方法AL-SMC.该方法采用了主成分分析、前缀树约减等技术,对仿真路径进行学习和抽象,以减少样本空间.接着,提出了一个面向CPS的自适应SMC算法框架,可根据不同的概率区间自动选择AL-SMC算法或者BIE算法,有效应对不同情况下的验证问题.最后,结合经典案例进行实验分析,实验结果表明自适应SMC算法框架能够在一定误差范围内有效提高CPSs统计模型检测的效率,为CPSs的分析验证提供了一种有效的途径.     

基于CREW遍历图的一种并行算法

针对串行算法模型下基于顶点遍历图的情况，提出了一种在CREWPRAM并行模型下遍历无向图的算法。该算法是找出无向图的一棵最短路径生成树，由向上和向下两条有向边替换最短路径生成树的每条边形成欧拉回路，运用欧拉回路技术计算前缀和，前缀和所对应的顶点即为遍历无向图的顺序。得出了该算法时间复杂度为O（n＋logn）的结论。     

统计算法选择对统计模型检测效率的影响分析

近年来,统计模型检测技术已经得到了广泛的应用,不同的统计算法对统计模型检测的性能有所影响。主要对比不同统计算法对统计模型检测的时间开销影响,从而分析算法的适用环境。选择的统计算法包括切诺夫算法、序贯算法、智能概率估计算法、智能假设检验算法及蒙特卡罗算法。采用无线局域网协议验证和哲学家就餐问题的状态可达性验证为实例进行分析,使用PLASMA模型检测工具进行验证。实验结果表明,不同的统计算法在不同的环境中对模型检测的效率有不同的影响。序贯算法适用于状态可达性性质的验证,时间性能最优;智能假设检验算法与蒙特卡罗算法适合验证复杂模型。这一结论有助于在模型检测时对统计算法的选择,从而提高模型检测的效率。     

OFDM中一种自适应盲均衡及改进算法

信道均衡在多载波系统中有很重要的应用.研究了OFDM信道自适应盲均衡问题,首先分析了Merry算法,基本思想是如果有效信道长度缩短到循环前缀长度以内,那么接收端符号具有和发送端符号一样的性质.但是Merry算法所构造的代价函数仅考虑了OFDM符号中循环前缀最后一个抽样与该符号最后一个抽样之间的关系.针对问题,构造了一个新的代价函数,利用了OFDM符号循环前缀中所有抽样的信息.文中对新算法进行了仿真验证,仿真结果表明,算法性能上明显要好于Merry算法.     

基于三值语义的软件运行时验证方法

运行时验证技术是对传统的程序正确性保证技术如模型检验和测试的有效补充。模型检验和测试都试图验证系统的所有可能执行路径的正确性,而运行时验证关注的是系统的当前执行路径。本文提出一种基于三值语义的软件运行时验证方法,一方面该方法提供了从代码插装、系统底层信息提取到监控器生成、验证系统运行轨迹是否满足性质规约的完整的解决方案;另一方面基于三值语义的监控器有发现一条无穷运行轨迹的最小好(坏)前缀的能力,从而使得监控器能尽可能早的发现性质违背。同时,我们开发了基于三值语义的软件运行时验证原型工具并针对案例进行了分析。     

移动卫星网络中的最短路径算法研究

移动卫星网络的拓扑时变性对其最短路径求解带来新的问题。文章利用提出的移动卫星网络模型，证明了基于传统网络的最短路径算法在移动卫星网络中使用存在局限性，提出了一种适用于移动卫星网络的最短路径求解方法和优化算法，并进行了仿真验证。     

基于梯度统计变异量子遗传算法的车辆路径规划

针对传统路径规划算法收敛速度慢、稳定性差、易陷入局部极值的问题, 提出一种基于梯度统计变异量子遗传算法的车辆路径规划方法. 首先在依据染色体适应度值动态调整旋转角步长的基础上, 引入梯度下降思想对量子旋转门调整策略进行改进; 根据染色体变化趋势的统计特性, 设计基于梯度统计的变异算子实现变异操作, 提出基于量子位概率密度的自适应变异策略; 以路径最短为指标建立车辆路径规划模型, 通过仿真实验验证改进算法在车辆路径规划中的有效性, 与其他优化算法相比, 本文改进算法所规划路径长度更短, 搜索稳定性更好, 能有效控制算法陷入局部最优.     

基于OpenFlow架构的域内源地址验证方法

源地址验证对网络安全、管理和计量都有重要意义.清华大学提出包括接入子网、域内和域间三个层次的源地址验证体系结构.其中域内用到一种基于集中计算路径的方法,但在传统网络环境限制下,其实现遇到很多问题.本文将利用软件定义网络对网络革新的便捷支持,基于OpenFlow网络对域内源地址验证方法进行重新设计与实现,并提出两种方案.一种是在已有路由表的基础上计算出域内任意两个子前缀间的路径并生成源地址前缀、目的地址前缀和入接口三元组作为过滤规则;另一种方案是重新设计新的路由算法,生成同时具有路由功能和验证源地址功能的四元组(源地址前缀、目的地址前缀、入接口和出接口)流表.并分别对两种方案做出对比,给出实验结果.     

基于抽样路径的K-匿名隐私保护算法

K-匿名是信息隐私保护的一种常用技术,而使用K-匿名技术不可避免会造成发布数据的信息损失,因此,如何提高K-匿名化后数据集的可用性一直以来都是K-匿名隐私保护的研究重点。对此提出了一种基于抽样路径的局域泛化算法——SPOLG算法。该算法基于泛化格寻找信息损失较小的泛化路径,为减少寻径时间,引入等概率抽样的思想,选用等概率抽样中的系统抽样方法进行取样,利用样本代替数据集在泛化格上寻找目标泛化路径,最后在该路径上对数据集进行泛化。同时,本算法使用局域泛化技术,能够降低信息损失量,提高发布数据集的可用性。实验结果证明,本算法匿名化的数据集信息损失度低,数据可用性高。     

基于稳定度的可信AS-IP宣告关系构建方法

互联网自治系统(AS)以在路由系统中宣告网络前缀的方式宣告IP地址块的所有权。当一个自治系统宣告了不属于它的网络前缀时,就会导致前缀劫持的发生。由于边界网关协议(BGP)本身无法验证AS和IP前缀之间的宣告关系是否真实,导致对前缀劫持的检测和判定异常困难。本文提出并实现一种基于稳定度的,构建可信AS-IP宣告关系的方法,并用于检测和判定前缀劫持。通过构建AS和IP前缀宣告关系的时间序列,计算该宣告关系在时间序列上的稳定度数值,并用于评估AS和IP前缀宣告关系的可信度。本文运用该方法对历史上发生过的大规模异常事件进行检测,实验表明,该方法能构造准确的AS和IP前缀宣告关系,并可有效地检测和判定前缀劫持事件。     

Model checking mobile ad hoc networks

Modeling arbitrary connectivity changes within mobile ad hoc networks (MANETs) makes application of automated formal verification challenging. We use constrained labeled transition systems as a semantic model to represent mobility. To model check MANET protocols with respect to the underlying topology and connectivity changes, we introduce a branching-time temporal logic. The path quantifiers are parameterized by multi-hop constraints over topologies, to discriminate the paths over which the temporal behavior should be investigated; the paths that violate the multi-hop constraints are not considered. A model checking algorithm is presented to verify MANETs that allow arbitrary mobility, under the assumption of reliable communication. It is applied to analyze a leader election protocol.     

Model checking temporal knowledge and commitments in multi-agent systems using reduction

Though modeling and verifying Multi-Agent Systems (MASs) have long been under study, there are still challenges when many different aspects need to be considered simultaneously. In fact, various frameworks have been carried out for modeling and verifying MASs with respect to knowledge and social commitments independently. However, considering them under the same framework still needs further investigation, particularly from the verification perspective. In this article, we present a new technique for model checking the logic of knowledge and commitments (CTLKC⁺). The proposed technique is fully-automatic and reduction-based in which we transform the problem of model checking CTLKC⁺ into the problem of model checking an existing logic of action called ARCTL. Concretely, we construct a set of transformation rules to formally reduce the CTLKC⁺ model into an ARCTL model and CTLKC⁺ formulae into ARCTL formulae to get benefit from the extended version of NuSMV symbolic model checker of ARCTL. Compared to a recent approach that reduces the problem of model checking CTLKC⁺ to another logic of action called GCTL¹, our technique has better scalability and efficiency. We also analyze the complexity of the proposed model checking technique. The results of this analysis reveal that the complexity of our reduction-based procedure is PSPACE-complete for local concurrent programs with respect to the size of these programs and the length of the formula being checked. From the time perspective, we prove that the complexity of the proposed approach is P-complete with regard to the size of the model and length of the formula, which makes it efficient. Finally, we implement our model checking approach on top of extended NuSMV and report verification results for the verification of the NetBill protocol, taken from business domain, against some desirable properties. The obtained results show the effectiveness of our model checking approach when the system scales up.     

Model Checking Semi-Continuous Time Models Using BDDs

The verification of timed systems is extremely important, but also extremely difficult. Several methods have been proposed to assist in this task, including extensions to symbolic model checking. One possible use of model checking to analyze timed systems is by modeling passage of time as the number of taken transitions and applying quantitative algorithms to determine the timing parameters of the system. The advantage of this method is its simplicity and efficiency. In this paper we extend this technique in two ways. First, we present new quantitative algorithms that are more efficient than their predecessors. The new algorithms determine the number of occurrences of events in all paths between a set of starting states and a set of final states. We then use these algorithms to introduce a new model of time, in which the passage of time is dissociated from the occurrence of events. With this new model it is possible to verify systems that were previously thought to require dense time models. We use the new method to verify two such examples previously analyzed by the HyTech tool: a steam boiler example and a fuel injection controller.     

一种自动化模型检测ANSI-C程序的实用方法

模型检测是一种验证有限状态系统的时序逻辑属性的形式化方法。为了利用模型检测技术,通常的办法是手工构建一个抽象模型,然而这个方法存在一些不足,如成本过高、易引入建模错误等。本文提出了一种自动化模型检测ANSI-C程序的方法,并开发了模型提取工具C2Spin,它能够分析ANSI-C源代码,并生成对应的PROMELA验证模型,从而显著降低了建模的开销。利用C2Spin,模型检测工具SPIN可以自动地检测使用C语言编写的应用程序中的多种错误,如死锁等。在初步实验中,依靠C2Spin生成的模型,我们发现了SPIN4.3.0的一个语义错误,以及Holzmann对两个经典互斥算法的实现程序中的活锁错误。这些结果表明,C2Spin能够帮助人们更加快速有效地测试C程序。     

Are the Logical Foundations of Verifying Compiler Prototypes Matching user Expectations?

The verifying compiler (VC) project proposals suggest that mainstream software developers are its targeted end-users. Like other software engineering efforts, the VC project success depends on appropriate end-user consultation. Industrial use of program assertions for the purpose of run-time assertion checking (RAC) is becoming commonplace. A likely next step on the path to VC adoption is the use of assertions in extended static checking (ESC), a fully automated form of static program verification (SPV). Unfortunately, all current VC prototypes supporting SPV, adopt a semantics which is unsound relative to the standard run-time interpretation of assertions. In this article, we report on the results of a survey in which we asked industrial developers what logical semantics they want program assertions to have, and whether consistency across RAC and SPV tools is important. Survey results indicate that developers are in favor of a semantics for assertions that is compatible with their current use in RAC.     

Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach

The state space explosion problem in model checking remains the chief obstacle to the practical verification of real-world distributed systems. We attempt to address this problem in the context of verifying concurrent (message-passing) C programs against safety specifications. More specifically, we present a fully automated compositional framework which combines two orthogonal abstraction techniques (operating respectively on data and events) within a counterexample-guided abstraction refinement (CEGAR) scheme. In this way, our algorithm incrementally increases the granularity of the abstractions until the specification is either established or refuted. Our explicit use of compositionality delays the onset of state space explosion for as long as possible. To our knowledge, this is the first compositional use of CEGAR in the context of model checking concurrent C programs. We describe our approach in detail, and report on some very encouraging preliminary experimental results obtained with our tool MAGIC.     

Verifying a quantitative relaxation of linearizability via refinement

The recent years have seen increasingly widespread use of highly concurrent data structures in both multi-core and distributed computing environments, thereby escalating the priority for verifying their correctness. Quasi linearizability is a quantitative variation of the standard linearizability correctness condition to allow more implementation freedom for performance optimization. However, ensuring that the implementation satisfies the quantitative aspect of this new correctness condition is often an arduous task. In this paper, we propose the first automated method for formally verifying quasi linearizability of the implementation model of a concurrent data structure with respect to its sequential specification. The method is based on checking a relaxed version of the refinement relation between the implementation model and the specification model through explicit state model checking. Our method can directly handle concurrent systems where each thread or process makes infinitely many method calls. Furthermore, unlike many existing verification methods, it does not require the user to supply annotations of the linearization points. We have implemented the new method in the PAT verification framework. Our experimental evaluation shows that the method is effective in verifying the new quasi linearizability requirement and detecting violations.     

Verification of complex dynamic data tree with mu-calculus

The problem of verifying software systems that use dynamic data structures (such as linked lists, queues, or binary trees) has attracted increasing interest over the last decade. Dynamic structures are not easily supported by verification techniques because, among other reasons, it is difficult to efficiently manage the pointer-based internal representation. This is a key aspect when, for instance, the goal is to construct a verification tool based on model checking techniques. In addition, since new nodes can be dynamically inserted or extracted from the structure, the shape of the dynamic data (and other more specific properties) may vary at runtime, with errors such as the non desirable sharing between two nodes being difficult to detect. In this paper, we propose to use mu-calculus to describe and analyze with model checking techniques dynamic data structures such as lists and trees. The expressiveness of mu-calculus makes it possible to naturally describe these structures. In addition, following the ideas of separation logic, the logic has been extended with a new operator capable of describing the non-sharing property, which is essential when analyzing dynamic data structures.     

Verifying concurrent probabilistic systems using probabilistic-epistemic logic specifications

In this paper, we address the problem of verifying probabilistic and epistemic properties in concurrent probabilistic systems expressed in PCTLK. PCTLK is an extension of the Probabilistic Computation Tree Logic (PCTL) augmented with Knowledge (K). In fact, PCTLK enjoys two epistemic modalities K_i for knowledge and \(Pr_{\triangledown b}K_{i}\) for probabilistic knowledge. The approach presented for verifying PCTLK specifications in such concurrent systems is based on a transformation technique. More precisely, we convert PCTLK model checking into the problem of model checking Probabilistic Branching Time Logic (PBTL), which enjoys path quantifiers in the range of adversaries. We then prove that model checking a formula of PCTLK in concurrent probabilistic programs is PSPACE-complete. Furthermore, we represent models associated with PCTLK logic symbolically with Multi-Terminal Binary Decision Diagrams (MTBDDs), which are supported by the probabilistic model checker PRISM. Finally, an application, namely the NetBill online shopping payment protocol, and an example about synchronization illustrated through the dining philosophers problem are implemented with the MTBDD engine of this model checker to verify probabilistic epistemic properties and evaluate the practical complexity of this verification.     

The role of model checking in software engineering

Model checking is a formal verification technique. It takes an exhaustively strategy to check hardware circuits and network protocols against desired properties. Having been developed for more than three decades, model checking is now playing an important role in software engineering for verifying rather complicated software artifacts.This paper surveys the role of model checking in software engineering. In particular, we searched for the related literatures published at reputed conferences, symposiums, workshops, and journals, and took a survey of (1) various model checking techniques that can be adapted to software development and their implementations, and (2) the use of model checking at different stages of a software development life cycle. We observed that model checking is useful for software debugging, constraint solving, and malware detection, and it can help verify different types of software systems, such as object- and aspect-oriented systems, service-oriented applications, web-based applications, and GUI applications including safety- and mission-critical systems.The survey is expected to help human engineers understand the role of model checking in software engineering, and as well decide which model checking technique(s) and/or tool(s) are applicable for developing, analyzing and verifying a practical software system. For researchers, the survey also points out how model checking has been adapted to their research topics on software engineering and its challenges.