共查询到20条相似文献,搜索用时 93 毫秒
1.
软件构件的可信保证研究 总被引:4,自引:0,他引:4
近年来,可信构件的研究逐渐引起软件工程领域的重视。可信构件研究与应用的目标是为了给基于构件的软件工程(CⅨ汇)提供坚实的基础,而方法就是通过扩展与完善可信重用的软件构件(可信构件)库。构件的可信来源于可信保障技术的应用,如:契约设计的使用、正确性的数学证明、软件测试、详细的代码走查、基于度量的评估、实际项目的验证、严格的变更管理等。本文通过分析可信构件研究的若干领域,总结出构件可信性的3个角度,探讨了可信构件研究的不足之处,并分析其原因。作为总结,给出了可信构件领域研究需要解决的若干问题。 相似文献
2.
3.
4.
基于时态逻辑的硬件设计形式化验证技术——模型检验 总被引:3,自引:0,他引:3
通过对时态逻辑的研究来探讨时态逻辑在硬件设计形式化验证上的应用,同时对布尔函数在计算机内的表示二叉判定图(BDD)进行了进一步地分析,最后给出了一个时态逻辑对硬件设计进行验证的例子。 相似文献
5.
6.
模型检验输出的反例提供了一种自动产生测试用例的有效途径。提出了一种用模型检验进行构件数据流测试的方法。利用构件状态机描述构件的外部行为,用带有变量定义和使用标记的Kripke结构描述构件状态迁移中的数据流信息;给出了从构件状态机到Kripke结构的转换方法,并建立了全定义覆盖和全使用覆盖准则的陷阱性质构造公式。陷阱性质将使模型检验器NuSMV输出反例,从而产生构件的数据流测试序列。 相似文献
7.
基于Petri网的协议并行化处理模型的描述和验证 总被引:3,自引:0,他引:3
本文提出了一个OSI/RM运输层协议并行处理模型,以适应协议的高效处理,根据模型特点,使用Petri网作为形式化描述工具,对该模型进行描述,分析和验证。 相似文献
8.
9.
基于自动机的构件实时交互行为的形式化模型 总被引:1,自引:1,他引:1
采用形式化方法对复杂实时构件系统交互行为进行描述和验证,对于提高系统的正确性、可靠性等可信性质具有重要意义.分析了基于进程代数和自动机的构件交互行为形式化建模方法各自的优缺点,在此基础上提出了基于时间构件交互自动机的建模方法,给出了时间构件交互自动机的相关定义、组合和验证算法.时间构件交互自动机引入了时间限制、时间代价、时间代价计算半环、构件组合层次等概念,既能够描述构件交互情况,又能够清楚地表示出构件系统的体系结构信息和实时信息,便于对系统进行描述和验证.最后,结合具体应用给出了应用示例. 相似文献
10.
并发和实时系统的模型检验技术 总被引:4,自引:1,他引:4
模型检验是一种重要的自动验证技术,通过显式状态搜索或隐式不动点计算来验证并发或实时系统的模态/命题性质,以保证通信协议、数字电路等设计的正确性。详细阐述了模型检验技术的发展与研究现状。首先描述了并发系统分别基于自动机理论和符号化的两种主要模型检验策略,并给出解决状态爆炸问题的主要方法;然后介绍了针对实时系统以及面向对象设计的模型检验方法;对每种方法都介绍了相应的典型工具,最后分析了模型检验面临的困难以及今后的发展趋势。 相似文献
11.
Shoham Ben-David Cindy Eisner Daniel Geist Yaron Wolfsthal 《Formal Methods in System Design》2003,22(2):101-108
Over the past nine years, the Formal Methods Group at the IBM Haifa Research Laboratory has made steady progress in developing tools and techniques that make the power of model checking accessible to the community of hardware designers and verification engineers, to the point where it has become an integral part of the design cycle of many teams. We discuss our approach to the problem of integrating formal methods into an industrial design cycle, and point out those techniques which we have found to be especially effective in an industrial setting. 相似文献
12.
13.
Web服务的模型检测技术探讨 总被引:1,自引:0,他引:1
从模型检测的基本概念出发,针对目前面向服务计算模式中,组合Web服务验证确认过程存在的问题,着重讨论了模型检测应用于Web服务验证中的关键技术,例如如何验证动态绑定服务的可信性,如何克服服务组合过程中的复杂性和不确定性;比较全面地总结并比较了几种具有代表性的对Web服务进行验证和确认的模型检测技术和相关工具;并探讨了应用于Web服务验证框架的模型检测技术研究中存在的一些问题及相应的解决方案. 相似文献
14.
Component Verification with Automatically Generated Assumptions 总被引:3,自引:0,他引:3
Model checking is an automated technique that can be used to determine whether a system satisfies certain required properties. The typical approach to verifying properties of software components is to check them for all possible environments. In reality, however, a component is only required to satisfy properties in specific environments. Unless these environments are formally characterized and used during verification (assume-guarantee paradigm), the results returned by verification can be overly pessimistic. This work introduces an approach that brings a new dimension to model checking of software components. When checking a component against a property, our modified model checking algorithms return one of the following three results: the component satisfies a property for any environment; the component violates the property for any environment; or finally, our algorithms generate an assumption that characterizes exactly those environments in which the component satisfies its required property. Our approach has been implemented in the LTSA tool and has been applied to the analysis of two NASA applications.This paper is an expanded version of Giannakopoulou et al. (2002). 相似文献
15.
Java bytecode verification is traditionally performed by using dataflow analysis. We investigate an alternative based on reducing
bytecode verification to model checking. First, we analyze the complexity and scalability of this approach. We show experimentally
that, despite an exponential worst-case time complexity, model checking type-correct bytecode using an explicit-state on-the-fly
model checker is feasible in practice, and we give a theoretical account why this is the case. Second, we formalize our approach
using Isabelle/HOL and prove its correctness. In doing so we build on the formalization of the Java Virtual Machine and dataflow
analysis framework of Pusch and Nipkow and extend it to a more general framework for reasoning about model-checking-based
analysis. Overall, our work constitutes the first comprehensive investigation of the theory and practice of bytecode verification
by model checking.
This revised version was published online in August 2006 with corrections to the Cover Date. 相似文献
16.
如今,越来越多的社会决策借助机器学习模型给出,包括法律决策、财政决策等等.对于这些决策,算法的公平性是极为重要的.事实上,在这些环境中引入机器学习的目的之一,就是为了规避或减少人类在决策过程中存在的偏见.然而,数据集常常包含敏感特征,或可能存在历史性偏差,会使得机器学习算法产生带有偏见的模型.由于特征选择对基于树的模型具有重要性,它们容易受到敏感属性的影响.提出一种基于概率模型检查的方法,以形式化验证决策树和树集成模型的公平性.将公平性问题转换为概率验证问题,为算法模型构建PCSP#模型,并使用PAT模型检查工具求解,以不同定义的公平性度量衡量模型公平性.基于该方法开发了FairVerify工具,并在多个基于不同数据集和复合敏感属性的分类器上验证了不同的公平性度量,展现了较好的性能.与现有的基于分布的验证器相比,该方法具有更高的可扩展性和鲁棒性. 相似文献
17.
Web服务组合是服务计算领域的重要研究内容。用户的非功能性需求是Web服务组合中衡量服务的标准之一,然而开放环境下用户的需求具有一定的不确定性和多目标性特点。为了解决此种不确定性,提出了一种基于概率模型检测的多目标验证方法。首先,将Web服务组合过程建立为定量多目标马尔可夫决策过程,并将该模型转换为PRISM模型。同时,将不同的用户需求建模成多目标时序逻辑公式,使用概率模型检测器PRISM对其进行验证,获得多个目标约束下关键目标的期望值,并导出相关策略。最后,通过实例来进一步说明该方法的有效性与可行性。 相似文献
18.
随着经济的发展和市场竞争的加剧,企业必须能够快速且准确地满足市场和用户的各种需求.Web服务组合正是由于单个Web服务不能满足企业及用户的需求而产生的一种技术,而如何确保组合的正确性来实现服务增值是一个尚未完全解决的问题.针对此问题,提出了一种基于符号模型检测器NuSMV对Web服务组合进行验证的方法,并提出了基于消息... 相似文献
19.
20.
Yael Abarbanel-Vinov Neta Aizenbud-Reshef Ilan Beer Cindy Eisner Daniel Geist Tamir Heyman Iris Reuveni Eran Rippel Irit Shitsevalov Yaron Wolfsthal Tali Yatzkar-Haham 《Formal Methods in System Design》2001,19(1):35-44
We examine IBM's exploitation of formal verification using RuleBase—a formal verification tool developed by the IBM Haifa Research Laboratory. The goal of the paper is methodological. We identify an integrated methodology for the deployment of formal verification which involves three complementary modes: architectural verification, block-level verification, and design exploration. 相似文献