共查询到19条相似文献,搜索用时 218 毫秒
1.
基于模型检测的时间空间性能验证方法 总被引:1,自引:0,他引:1
对具有不确定性的复杂系统如网络协议等的性能进行分析是当前的研究热点.将空间资源分析纳入到性能评估过程,用模型检测技术验证时间或空间性能是否满足期望的需求约束.用能刻画不确定性的连续时间Markov回报过程(Continuous-Time Markov Reward Process,CTMRP)作为时间或空间性能验证模型;用正则式表示路径约束,扩展连续随机回报逻辑CSRL(Continuous Stochastic Reward Logic)的时态路径算子,用以刻画更加广泛的基于状态或路径的时间或空间性能验证属性;提出并证明CTMRP在确定性策略下空间时间可达概率的对偶性质,将带有约束的空间性能验证最终转化为时间性能的可达分析,给出验证算法.文中的结论和算法为复杂系统的性能分析提供了新的思路和方法. 相似文献
2.
对复杂信息系统的功能、性能进行组合验证,进而评估系统是否安全、可信,是当前的研究热点,但目前缺乏增加空间约束的验证模型.文章扩展已有的功能、性能验证模型,在状态空间上定义空间要求函数,提出一种刻画功能、时间和空间性能的统一验证模型atsFPM.给出基于正则式的路径范式描述信息系统行为的功能属性,给出atsFPM模型的语法和语义,构造路径范式与系统模型的积自动机,证明积自动机与原始模型在功能刻画、时间和空间描述上的等价,提出针对atsFPM的功能性能组合模型验证算法.实例分析表明,atsFPM统一验证模型能够有效解决信息系统功能和性能的组合分析问题,确保系统正确、安全、可信. 相似文献
3.
4.
为实现安全高效的版权授权交易,使原创版权作品得到有效保护。针对区块链技术中的共识机制加以改进,提出一种适应可信版权登记与授权交易场景的DPOS共识机制改进方法。基于信用值和币龄进行设计,采用CES生产函数模型对节点可信程度进行衡量,减少作恶节点当选代表节点的概率;通过基于混合同余算法的随机出块策略和新型区块合法性验证策略,实现区块可信的产生与验证过程,增强共识算法安全性;增加基于出块时间的信用值奖惩机制,增大网络带宽与节点性能更好的节点成为出块节点的概率,提升系统效率。实验结果表明,改进方案可以全面提升区块链系统的安全性和效率,有效应用在版权交易领域,实现可信的版权授权交易。 相似文献
5.
AIFS 区分的IEEE 802.11e EDCA 吞吐率分析模型与自适应MAC 算法 总被引:1,自引:1,他引:0
针对IEEE 802.11e EDCA(enhanced distributed channel access)支持业务区分服务的特点,提出了一个基于AIFS(arbitration inter-frame space)区分的信道吞吐率分析模型,该模型将不同接入等级的业务统一到一个信道模型中进行分析.通过数值计算结果与仿真实验结果的对比,验证了该模型的准确性,尤其是在分析信道吞吐率方面更优于Xiao 的Markov 链模型.根据提出的分析模型,研究了近似优化条件,使得各类优先级业务的发送概率平衡虚拟发
送时间段中空闲时间与冲突持续时间对系统性能的影响,实现靠近最优的信道吞吐率,从而使计算复杂度大为减小.
利用数值分析的方法验证了近似优化条件实现靠近最优信道吞吐率的可行性.最后,提出的DPS(dynamicparameter-tuning scheme)算法根据负载情况自适应地调整不同级别业务的相应参数,使得系统时时满足优化条件,在各种场景下都能实现最大信道吞吐率,同时又满足EDCA 支持QoS 区分的要求.仿真结果验证了DPS 算法不仅能够根据竞争节点的数目变化对信道吞吐率进行优化,而且其性能也明显优于标准的IEEE 802.11e EDCA 机制. 相似文献
6.
7.
8.
可信动态度量为保障可信计算平台的可靠运行提供了重要支撑.根据系统的可靠性、可用性、信息和行为安全性,提出了可信度量要达到的目标.当前的可信度量集中在可信功能度量上,基于交互式马尔可夫链增加性能特征指标度量,即在预期行为描述模型中,运用变迁系统模型描述功能预期,通过将体现在可靠性上的路径概率与预期的关联,获取完成特定行为... 相似文献
9.
在Internet动态、开放、异构、多变的环境下,组合式软件不仅要满足功能正确,非功能(时间、代价、概率等)属性的满足也日益成为一个重要的问题。在组合式软件的设计阶段,建立组合式软件功能和非功能的统一模型并验证其功能正确性和非功能满足性,是确保组合式软件可信性的重要手段。在UML序列图的基础上进行时间、代价、概率属性的扩展,提出了一种可对组合式软件的交互行为及其时间、代价、概率属性统一建模的属性序列图,该属性序列图以两层模式进行建模,其中基本属性序列图可对涉及时间、代价属性的具体交互场景建模,高层属性序列图通过概率合成基本属性序列图可形成全局场景。给出了针对BPEL4WS的建模实例以说明所提建模方法的有效性。 相似文献
10.
在M/M/1/N可修排队系统中引入了工作故障和启动时间.服务台在忙期允许出现故障,且在故障期间不是完全停止服务而是以较低的服务速率为顾客服务.同时,从关闭期到正规忙期有服从指数分布的启动时间.通过分析此模型的二维连续时间Markov过程,求解出系统平稳方程,建立此系统的有限状态拟生灭过程(QBD).根据系统参数,求解出水平相依的子率阵,从而得到系统稳态概率向量的矩阵几何表示形式.在系统稳态概率向量的基础上,求解出系统吞吐率、系统稳态可用度、系统稳态队长及系统处于各个状态的概率等性能指标的解析表达式.文中的敏感性分析体现了这种方法的有效性和可用性,同时,对系统各性能受系统参数的影响进行了探索.实验表明,文中提出模型的稳定性较好,且更贴近实际服务过程,因此这种模型将被广泛应用于各种实际服务中. 相似文献
11.
当前缺乏对聚合云服务正确性、响应时间和费用约束统一进行验证的有效方法。扩展基本工作流模式,增强概率、随机、不确定选择的刻画能力,用于定义聚合云服务的服务流程,将流程定义转换为连续时间Markov回报过程,扩展连续随机回报逻辑CSRL,用以刻画增强行为描述的统一验证属性,给出随机模型检测方法。分析表明,该方法能有效刻画运行时云服务动态行为并对其正确性、可靠性进行验证。 相似文献
12.
Modeling and formal verification of embedded systems based on a Petri net representation 总被引:2,自引:0,他引:2
In this paper we concentrate on aspects related to modeling and formal verification of embedded systems. First, we define a formal model of computation for embedded systems based on Petri nets that can capture important features of such systems and allows their representation at different levels of granularity. Our modeling formalism has a well-defined semantics so that it supports a precise representation of the system, the use of formal methods to verify its correctness, and the automation of different tasks along the design process. Second, we propose an approach to the problem of formal verification of embedded systems represented in our modeling formalism. We make use of model checking to prove whether certain properties, expressed as temporal logic formulas, hold with respect to the system model. We introduce a systematic procedure to translate our model into timed automata so that it is possible to use available model checking tools. We propose two strategies for improving the verification efficiency, the first by applying correctness-preserving transformations and the second by exploring the degree of parallelism characteristic to the system. Some examples, including a realistic industrial case, demonstrate the efficiency of our approach on practical applications. 相似文献
13.
Parthasarathy G. Iyer M.K. Cheng K.-T. Wang L.-C. 《Design & Test of Computers, IEEE》2004,21(2):132-143
Model checkers verify properties of safety- or business-critical systems. The main idea behind model checking is to convert a design's verification into a problem of checking key design properties expressed as a set of temporal logic formulas. The graph representing the design's state space then becomes the basis for testing these formulas' satisfiability (SAT). This divide-and-conquer approach provides an overall test for design correctness. We describe a method for checking safety properties using sequential SAT. SSAT can efficiently prove true properties by harnessing the power of bounded model checking (BMC) using SAT, but without the need for a pre-computed correctness threshold. Using a standard set of benchmarks, we conducted experiments to compare the runtime behavior of SSAT with BMC and binary decision diagrams (BDDs). 相似文献
14.
Tsuchiya T. Nagano S. Paidi R.B. Kikuno T. 《Parallel and Distributed Systems, IEEE Transactions on》2001,12(1):81-95
A distributed system is said to be self-stabilizing if it converges to safe states regardless of its initial state. In this paper we present our results of using symbolic model checking to verify distributed algorithms against the self-stabilizing property. In general, the most difficult problem with model checking is state explosion; it is especially serious in verifying the self-stabilizing property, since it requires the examination of all possible initial states. So far applying model checking to self-stabilizing algorithms has not been successful due to the problem of state explosion. In order to overcome this difficulty, we propose to use symbolic model checking for this purpose. Symbolic model checking is a verification method which uses Ordered Binary Decision Diagrams (OBDDs) to compactly represent state spaces. Unlike other model checking techniques, this method has the advantage that most of its computations do not depend on the initial states. We show how to verify the correctness of algorithms by means of SMV, a well-known symbolic model checker. By applying the proposed approach to several algorithms in the literature, we demonstrate empirically that the state spaces of self-stabilizing algorithms can be represented by OBDDs very efficiently. Through these case studies, we also demonstrate the usefulness of the proposed approach in detecting errors 相似文献
15.
Tolga Ovatman Atakan Aral Davut Polat Ali Osman Ünver 《Software and Systems Modeling》2016,15(4):937-960
Programmable logic controllers (PLCs) are heavily used in industrial control systems, because of their high capacity of simultaneous input/output processing capabilities. Characteristically, PLC systems are used in mission critical systems, and PLC software needs to conform real-time constraints in order to work properly. Since PLC programming requires mastering low-level instructions or assembly like languages, an important step in PLC software production is modelling using a formal approach like Petri nets or automata. Afterward, PLC software is produced semiautomatically from the model and refined iteratively. Model checking, on the other hand, is a well-known software verification approach, where typically a set of timed properties are verified by exploring the transition system produced from the software model at hand. Naturally, model checking is applied in a variety of ways to verify the correctness of PLC-based software. In this paper, we provide a broad view about the difficulties that are encountered during the model checking process applied at the verification phase of PLC software production. We classify the approaches from two different perspectives: first, the model checking approach/tool used in the verification process, and second, the software model/source code and its transformation to model checker’s specification language. In a nutshell, we have mainly examined SPIN, SMV, and UPPAAL-based model checking activities and model construction using Instruction Lists (and alike), Function Block Diagrams, and Petri nets/automata-based model construction activities. As a result of our studies, we provide a comparison among the studies in the literature regarding various aspects like their application areas, performance considerations, and model checking processes. Our survey can be used to provide guidance for the scholars and practitioners planning to integrate model checking to PLC-based software verification activities. 相似文献
16.
由于自动柜员机需要提供可靠的服务,确保其业务逻辑的正确性具有非常重要的意义.然而,传统的测试方法不能对其正确性进行验证.以相关业务逻辑为具体实例,给出一种基于Spin( Simple Promela Interpreter,一种典型的模型检测工具)的自动柜员机的模型检测方法.介绍如何对自动柜员机业务逻辑进行建模、如何对其主要属性进行描述和验证.实验结果表明了所提方法的可行性. 相似文献
17.
18.
Gopinadh Sirigineedi Antonios Tsourdos Brian A. White Rafał Żbikowski 《Annals of Mathematics and Artificial Intelligence》2011,63(1):31-52
A verifiable multiple UAV system cooperatively monitoring a road network is presented in this paper. The focus is on formal
modelling and verification which can guarantee correctness of concurrent reactive systems such as multi-UAV systems. Kripke
modelling is used to formally model the distributed cooperative control strategy, and to verify correctness of the specifications.
Desirable properties of the mission such as liveness are specified in Computation Tree Logic (CTL). Model checking technique
is used to exhaustively explore the state space to verify whether the system behaviour, modelled by Kripke model, satisfies
the specifications. Violation of a specification is analysed by means of the counter-example generated by SMV model checking
tool. 相似文献
19.
In this paper we propose an automatic methodology to verify the soundness of model checking reduction techniques. The idea is to use the consistency of the specifications to verify if the reduced model is faithful to the original one. The user provides the reduction technique, the specification and the system under verification. Then, using Higher Order Logic he verifies automatically if the reduction technique is soundly applied. The method is completely defined in an MDG–HOL special integration platform that combines an automatic high level model checking tool Multiway Decision Graphs (MDGs) within the HOL theorem prover. We provide two case studies, the first one is the reduction using SAT–MDG of an Island Tunnel Controller and the second one is the MDG–HOL assume-guarantee reduction of the Look-Aside Interface. The obtained results of our approach offer a considerable gain in terms of the correctness of heuristics and reduction techniques as applied to commercial model checking, however a small penalty is paid in terms of CPU time and memory usage. 相似文献