循环对称化简及在三值模型上的扩展

为了将对称化简扩展到更多的非对称系统上,扩展了传统的基于自同构的对称性,提出了一种称为循环对称的新的对称性.证明了采用循环对称置换群或者由一组循环对称置换所生成的置换群仍可得到与原模型互模拟的对称商结构,从而达到化简系统规模的目的.进一步地,研究如何将对称化简应用于多值模型.多值模型可以有效地表示系统中的不确定信息,正越来越多地用于软件系统的建模与分析中.针对一种具体的多值模型——三值模型,定义传统的对称化简和循环对称化简在其上面的扩展.最后,分析三值模型的商结构与由约简得到的二值模型商结构之间的关系,证明了两种途径的等价性.     

基于分解的多值模型的逼近关系

多值模型可用于对包含不确定与不一致信息的软件系统进行建模与验证。提出了采用基于分解的方式来刻画多值模型之间的逼近关系,这为采用抽象方法解决模型检测时所产生的状态爆炸问题奠定了理论基础。为此,首先给出了多值模型分解为多个三值模型的方法,并且证明了任意μ演算公式在多值模型上的检测结果等于在分解后所有三值模型上的检测结果的合并。进一步,由三值模型上的混合模拟关系给出了多值模型间逼近关系的结构定义,并证明对于任意给定的两个满足逼近关系的多值模型,μ演算公式在其上的检测结果在信息序关系上得以保持。     

一种从面向对象Z规约到代码的精化演算方法

COOZ(complete object-oriented Z)的优势在于精确描述大型程序的规约.COOZ本身的结构 不支持精化演算,这限制了COOZ的应用能力,使COOZ难以作为完整的方法应用于软件的开发. 将精化演算引入COOZ,弥补了COOZ在设计和实现阶段的不足,同时也消除了规约与实现之间在 结构和表示方法上的完全分离,使程序开发在一个完整的框架下平滑进行.该文提出了基于CO OZ和精化演算的软件开发模型,通过实例讨论了数据精化和操作精化问题.在精化演算实现技 术方面构造了一种数据精化算子,提出一     

精化演算支撑工具的分析

利用精化演算的方法开发软件,其过程由巨大数量的小步骤构成,由手工完成极其烦琐,也极容易出错。因此,利用机器辅助工具的支持是必要的。在分析现有的精化工具的基础上,我们提出了一个用于软件形式化开发的精化工具RT(RefinementTool),对精化工具进行了需求分析和功能分析。在精化工具的设计中,分析了精化工具的设计目标、总体结构、精化与证明的表示方法、用户界面和工具的扩充性等问题,通过对精化和证明的表示方法的分析,提出了一种精化与证明的表示相结合的方法。     

模糊计算树逻辑的符号模型检测

对含有模糊不确定性信息的系统进行模型检测时,状态空间爆炸问题成为了亟待解决的主要问题.将形式化的系统模型用拟布尔公式表示,用多终端二叉决策图来对拟布尔公式进行存储.对模糊计算树逻辑的不动点语义给出了解释和证明,然后给出模糊计算树逻辑的符号化模型检测算法,最后通过一个实例验证算法的正确性.该算法可有效缓解对模糊模型检测验证时的状态空间爆炸问题,并扩展了模型检测的应用范围.     

精化演算支撑工具PRT的研究

1 引言精化演算是一种数学表示法和若干规则的集合,用于从程序规约推导出命令式程序。精化是从抽象程序向具体程序转换的过程,其中包含程序的正确性证明。精化的程序开发方法比对已有程序进行验证以保证程序正确性的方法更有效。通过精化演算中的转换规则可以演算出精化的程序。利用精化演算从规约导出程序的过程由大量步骤构成,非常适合利用机器工具进行辅助。本文对精化工具进行了需求分析和功能分析,研究了一个新的精化工具PRT(Program Refinement Tool)并与现有的一些工具进行了比较。     

布尔函数的计算机化简

一、引言 布尔函数的化简方法有三个:公式法;图解法;用计算机化简布尔函数,这是最有力的方法。本文将介绍其基本原理,并辅之以解题实例和程序框图,便于读者了解有关内容。 多输出函数的化简比单输出函数的化简具有更大的实用价值。因为在一个复杂的数字系统中会有许多个布尔函数,如果把每个函数单独进行化简而不是当作一个整体加以考虑,就会大大增加成本。而人同时顾及多个函数的能     

模态逻辑公式的真度理论

在模态逻辑系统中,对可能世界进行了深入的分析,首次提出了完整模型的概念,并且在这个完整模型的框架下定义了模态公式的真度概念,建立了公式的真度理论。并且证明了：若模态公式[φ]不含任何模态词,即经典逻辑公式,它对应的模态真度[τ(φ)]就由区间退化为一个点,并且这个点就是该公式的Borel型真度值。     

对称布尔函数的算术相关函数

算术相关函数是最近提出的一种研究布尔函数密码学性质的方法,该方法通过定义多元2-adic数上的加法和乘法运算,构建一种新的环结构,实现对经典相关函数的带进位计算的模拟。首先介绍了算术相关函数的定义,并针对具有良好密码学性质的对称布尔函数讨论了其算术相关函数的性质和取值,最后利用对称布尔函数的实值对称性证明了对称布尔函数的算术自相关函数也是一个与向量的重量有关的实值对称函数,至多是n+1值的。     

一种基于构件演算的主动构件精化方法

现代构件系统通常包含多个并发执行的主动构件,这使得验证构件系统的正确性变得十分困难.通过对构件演算进行扩展,提出了一种主动构件的精化方法.在构件接口层引入契约.契约使用卫式设计描述公共方法和主动活动的功能规约.通过一对发散、失败集合定义契约的动态行为,并利用发散、失败集合之间的包含关系定义契约间的精化关系.证明了应用仿真技术确认契约精化关系的定理.定义构件的语义为其需求接口契约到其服务接口契约的函数,以此为基础,可以通过契约的精化来证明构件的精化.给出了构件的组装规则.在构件系统自底向上的构造过程中,应用构件的精化方法和组装规则可以保证最终系统的正确性.     

Temporal logic query checking: a tool for model exploration

Temporal logic query checking was first introduced by W. Chan in order to speed up design understanding by discovering properties not known a priori. A query is a temporal logic formula containing a special symbol ?/sub 1/, known as a placeholder. Given a Kripke structure and a propositional formula /spl phi/, we say that /spl phi/ satisfies the query if replacing the placeholder by /spl phi/ results in a temporal logic formula satisfied by the Kripke structure. A solution to a temporal logic query on a Kripke structure is the set of all propositional formulas that satisfy the query. Query checking helps discover temporal properties of a system and, as such, is a useful tool for model exploration. In this paper, we show that query checking is applicable to a variety of model exploration tasks, ranging from invariant computation to test case generation. We illustrate these using a Cruise Control System. Additionally, we show that query checking is an instance of a multi-valued model checking of Chechik et al. This approach enables us to build an implementation of a temporal logic query checker, TLQSolver, on top of our existing multi-valued model checker /sub /spl chi//Chek. It also allows us to decide a large class of queries and introduce witnesses for temporal logic queries-an essential notion for effective model exploration.     

并发反应式系统的组合模型检验与组合精化检验

模型检验和精化检验是两种重要的形式验证方法,其应用的主要困难在于如何缓解状态爆炸问题.基于分而治之的思想进行组合模型检验和组合精化检验是应对这个问题的重要方法,它们利用系统的组合结构对问题进行分解,通过对各子系统性质的检验和综合推理导出整个系统的性质.在一个统一的框架下对组合模型检验和组合精化检验作了系统的分析和归纳,从模块检验的角度阐述了上述两种组合验证方法的原理及其相应的组合验证策略.同时总结了各类问题的复杂性,并对上述两种方法作了比较分析,揭示了它们之间的内在联系.最后展望了组合模型检验与组合精化检验的发展方向.     

Abstraction and approximation in fuzzy temporal logics and models

Recently, by defining suitable fuzzy temporal logics, temporal properties of dynamic systems are specified during model checking process, yet a few numbers of fuzzy temporal logics along with capable corresponding models are developed and used in system design phase, moreover in case of having a suitable model, it suffers from the lack of a capable model checking approach. Having to deal with uncertainty in model checking paradigm, this paper introduces a fuzzy Kripke model (FzKripke) and then provides a verification approach using a novel logic called Fuzzy Computation Tree Logic* (FzCTL*). Not only state space explosion is handled using well-known concepts like abstraction and bisimulation, but an approximation method is also devised as a novel technique to deal with this problem. Fuzzy program graph, a generalization of program graph and FzKripke, is also introduced in this paper in consideration of higher level abstraction in model construction. Eventually modeling, and verification of a multi-valued flip-flop is studied in order to demonstrate capabilities of the proposed models.     

具有多值决策过程的广义可能性计算树逻辑模型检测

模型检测是一种自动验证软硬件系统行为的有效技术。为了对包含非确定性信息、不一致信息的并发系统进行形式化验证,在可能性理论、多值逻辑的基础上,研究了具有多值决策过程的广义可能性多值计算树逻辑模型检测算法,及其在检验非确定性系统中的具体应用。首先构造了多值决策过程作为系统模型,用多值计算树逻辑描述系统属性。然后给出具有多值决策过程的广义可能性多值计算树逻辑的模型检测算法,该算法将模型检测的具体问题转换为多项式时间内的模糊矩阵运算。最后就包含非确定性选择的多值系统的模型检测问题,给出一个具体的应用实例。     

支持协商的网构软件体系结构行为建模与验证

针对网构软件行为中的不确定性和不完整性,提出了一种支持协商的网构软件体系结构行为建模与验证方法.在建模中,该方法借鉴了UML时序图元素表示法,并增加了建模元素支持行为的不确定与不完整建模.在验证中,除了集成广泛应用的模型检查工具Spin以提供行为模型的验证能力以外,还引入了基于反例引导的抽象-精化过程思想的协商检查,以解决不确定和不完整建模所带来的正确性验证问题.     

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

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

基于模拟关系的精化检测方法

精化检测是一种重要的形式化验证方法,将系统实现和性质规约用相同形式化语言进行建模,如能证明两者间存在某种精化关系且该关系能够维持性质,可得出系统实现满足性质规约.为验证不同类型的系统性质, traces、stable failures和failures-divergence精化检测方法已被提出.精化检测算法依赖于子集构造,因而其面临状态空间爆炸问题.近年来,已有学者针对NFA语言包含问题提出了基于模拟关系的状态空间消减方法,大大提高了算法性能,且该方法能直接用于traces精化检测.在此基础上,本文提出了基于模拟关系的stable failures和failures-divergence精化检测方法.此外,本文还将精化检测扩展到了时间系统的验证中,提出了基于模拟关系的时间自动机traces精化检测方法.实验结果表明,基于模拟关系的算法效率有很大提高.     

When not losing is better than winning: Abstraction and refinement for the full μ-calculus

This work presents a novel game-based approach to abstraction-refinement for the full μ-calculus, interpreted over 3-valued semantics.A novel notion of non-losing strategy is introduced and exploited for refinement. Previous works on refinement in the context of 3-valued semantics require a direct algorithm for solving a 3-valued model checking game. This was necessary in order to have the information needed for refinement available on one game board. In contrast, while still considering a 3-valued model checking game, here we reduce the problem of solving the game to solving two 2-valued model checking (parity) games. In case the result is indefinite (don’t know), the corresponding non-losing strategies, when combined, hold all the information needed for refinement. This approach is beneficial since it can use any solver for 2-valued parity games. Thus, it can take advantage of newly developed such algorithms with improved complexity.     

An Efficient and Scalable Approach to Correct Class Model Refinement

Today, programmers benefit immensely from Integrated Development Environments (IDEs), where errors are highlighted within seconds of their introduction. Yet, designers rarely benefit from such an instant feedback in modeling tools. This paper focuses on the refinement of UML-style class models with instant feedback on correctness. Following the Model-Driven Architecture (MDA) paradigm, we strongly believe in the benefit of maintaining high-level and low-level models separately to 1) document the lower level model and 2) continuously ensure the correctness of the low-level model during later evolution (i.e., high- or low-level models may be evolved independently). However, currently the refinement and subsequent evolution lack automated support, let alone an instant feedback on their correctness (i.e., consistency). Traditional approaches to consistency checking fail here because of the computational cost of comparing class models. Our proposed instant approach first transforms the low-level model into an intermediate model that is then easier comparable with the high-level model. The key to computational scalability is the separation of transformation and comparison so that each can react optimally to changes—changes that could happen concurrently in both the high- and low-level class models. We evaluate our approach on eight third-party design models. The empirical data show that the separation of transformation and comparison results in a 6 to 11-fold performance gain and a ninefold reduction in producing irrelevant feedback. While this work emphasizes the refinement of class models, we do believe that the concepts are more generally applicable to other kinds of modeling languages, where transformation and subsequent comparison are computationally expensive.