共查询到17条相似文献,搜索用时 62 毫秒
1.
为了方便证明程序的正确性,引入了Kripke结构,提出基于Kripke结构的程序正确性证明。重新定义了适合证明的Kripke结构,并描述了将程序流程图转换为Kripke结构状态图的方法。给出了证明程序正确性的相关定理和基于Kripke结构的程序正确性证明方法。证明方法为:首先,把程序流程图转换为状态图;然后,根据状态之间的转移关系列出每个状态下的状态谓词;最后,证明每个状态谓词为真。根据状态谓词进行证明,能够反映出程序执行的状态。用该方法对一个实例进行了完整的证明。 相似文献
2.
在过去的20年里,基于Kdpkc语义结构的模型检测技术在集成电路设计,网络协议分析,程序正确性验证及程序错误发现等方面证明了其有效性和能力.最近,在诸如使用SAT分析工具、有界模型检测等避免OBDDs的模型检测研究方面取得了相当大的进展提出的动态Knpke 语义结构是让原子命题集合AP可以改变.基于这个方法,提出了一个直接模型检测算法. 相似文献
3.
多值模型检测是解决形式化验证中状态爆炸问题的一种重要方法,三值模型检测是多值模型检测的基础,其中如何检验不确定状态的真值是一难点。针对不确定状态检验,提出了一种模型检测方法,首先对不完全Kripke结构PKS进行了扩展,然后在扩展后的模型上给出了检测不确定状态真值的方法,最后给出了基于扩展不完全Kripke结构的三值逻辑模型检测算法。与已有的三值逻辑模型检测算法相比,该算法降低了算法复杂度,完善了对于不确定或不一致信息的处理,从而增强了三值逻辑模型检测的实用性。 相似文献
4.
基于不完全Kripke结构三值逻辑的模型检验 总被引:2,自引:0,他引:2
模型检验技术是形式化验证中比较成熟的技术,但随着设计系统规模的增加,状态爆炸已成为其发展的一个主要问题.为解决此问题,本文提出对系统进行抽象,建立不完全的状态模型,在此状态模型上来验证表示其属性的逻辑公式.这样一个逻辑公式的真值除了真、假外,还出现了第三种情况:未知,即在这个状态模型下无法确定其真值,需要更多的状态信息才能确定.本文还讨论了二值逻辑的模型检验技术,在此基础上给出了基于不完全状态空间的三值逻辑的模型检验算法,此算法与二值逻辑模型检验算法相比,没有带来时间复杂度的增加,最后给出了三值逻辑模型检验算法的应用. 相似文献
5.
6.
本文将[1]一个重要定理(见本文命题2)提升为一个函子F:Insc→(Thc)op,并得到了该函子的余连续性和连续性。这为计算机的共享程序的安全调用以及模块化程序的再用技术的实现提供了一定的理论依据.同时也构造了一个liberal理论范畴TH1,这为“逐步求精”法处理参数化数据类型提供了依据,并且将命题2推广到TH1上。 相似文献
7.
1引言由于在实际过程中,要确定系统过程噪声的统计分布特性非常困难,因此研究系统噪声统计分布特性未知但有上界情况下的模型结构确定问题是非常有意义的,但迄今为止有界噪声情况下模型结构的确定方法还很少[1].Belforte,Bona,Cerone[2]提... 相似文献
8.
分配的序列效应代数(简记为DSEA),是指在一个效应代数上带有一种乘积运算并满足一定的条件。介绍了分配的序列效应代数中的左理想、右理想、理想、素理想和同余等概念,并且证明了满足(RDP)性质并且以1为乘积单位的分配序列效应代数是具有(RDP)性质的反格分配序列效应代数的子直积。 相似文献
9.
10.
11.
This paper proposes a new model, named cycle-weighted Kripke structure (CWKS), based on the traditional Kripke structure. It adds two integer weights to some transitions of the Kripke structure, restricting when these transitions can occur. These weights mainly specify the occurrences of some cycles in a Kripke structure, giving a range of how many times these cycles may be executed repeatedly. This new model can efficiently describe some quantitative discrete-time characters of reactive and concurrent systems, so it is significant for some model checking problems. We also define a subset of CWKS, named conditional CWKS, which satisfies a constraint referring to the weighted transitions in the structure. The paper modifies the explicit computation tree logic (CTL) model checking algorithm to accommodate the conditional CWKS. It can also be regarded as the foundation of some more complex models obtained by extending from the Kripke structure, which will be studied in the future. 相似文献
12.
State space minimization techniques are crucial for combating state explosion. A variety of explicit-state verification tools use bisimulation minimization to check equivalence between systems, to minimize components before composition, or to reduce a state space prior to model checking. Experimental results on bisimulation minimization in symbolic model checking contexts, however, are mixed. This paper explores bisimulation minimization as an optimization in symbolic model checking of invariance properties. We consider three bisimulation minimization algorithms. From each, we produce a BDD-based model checker for invariant properties and compare this model checker to a conventional one based on backwards reachability. Our comparisons, both theoretical and experimental, suggest that bisimulation minimization is not viable in the context of invariance verification, because performing the minimization requires as many, if not more, computational resources as model checking the unminimized system through backwards reachability. 相似文献
13.
计算机科学中的共代数方法的研究综述 总被引:5,自引:1,他引:4
代数理论已经在抽象数据类型、程序语义等计算机科学领域有了广泛的应用,而代数的对偶概念--共代数,则直到20世纪90年代中后期才被越来越多的计算机学者关注.代数从"构造"的角度研究数据类型,而共代数则从"观察"的角度考察系统及其性质.共代数方法对研究基于状态的系统有独特的优越性,可以对系统的行为等价、不确定性等从数学上进行深入的探讨.目前,共代数理论已经逐步应用在自动机理论、并发程序的语义、面向对象程序的规范等领域.对共代数的基本概念、范畴理论基础、共代数逻辑及应用等方面的最新研究成果进行了介绍,以引起国内相关研究领域的学者对计算机科学中的共代数方法的关注. 相似文献
14.
15.
Every endofunctor F of Set has an initial algebra and a final coalgebra, but they are classes in general. Consequently, the endofunctor F∞ of the category of classes that F induces generates a completely iterative monad T. And solutions of arbitrary guarded systems of iterative equations w.r.t. F exist, and can be found in naturally defined subsets of the classes TY.More generally, starting from any category
, we can form a free cocompletion
∞ of
under small-filtered colimits (e.g., Set∞ is the category of classes), and we give sufficient conditions to obtain analogous results for arbitrary endofunctors of
. 相似文献
16.
Adnan Aziz Thomas Shiple Vigyan Singhal Robert Brayton Alberto Sangiovanni-Vincentelli 《Formal Methods in System Design》2002,21(2):193-224
We present a polytime computable state equivalence that is defined with respect to a given CTL formula. Since it does not attempt to preserve all CTL formulas, like bisimulation does, we can expect to compute coarser equivalences. This equivalence can be used to reduce the complexity of model checking a system of interacting FSMs. Additionally, we show that in some cases our techniques can detect if a formula passes or fails, without forming the entire product machine. The method is exact and fully automatic, and handles full CTL. 相似文献
17.
Norihiro Kamide 《Journal of Logic, Language and Information》2002,11(4):453-470
We introduce Kripke semantics for modal substructural logics, and provethe completeness theorems with respect to the semantics. Thecompleteness theorems are proved using an extended Ishihara's method ofcanonical model construction (Ishihara, 2000). The framework presentedcan deal with a broad range of modal substructural logics, including afragment of modal intuitionistic linear logic, and modal versions ofCorsi's logics, Visser's logic, Méndez's logics and relevant logics. 相似文献