选择公理与Tukey引理等价性的机器证明

基于计算机证明辅助工具Coq,提出一种选择公理与Tukey引理等价性的形式化证明.在公理化集合论形式化系统基础上,给出选择公理与Tukey引理的形式化描述,这是Tukey引理的首次形式化.完成了选择公理与Tukey引理等价性的证明代码,并在Coq中通过验证.体现了基于Coq的数学定理机器证明具有可读性和交互性的特点,其证明过程规范、严谨、可靠,在集合论、拓扑学和代数学的形式化构建中具有重要应用.     

安全协议形式化分析方法

安全协议的形式化分析是检验协议安全性的必要手段。为了实现协议的规范描述和合理完备的安全性验证,各种数学理论和人工智能方法被引进安全协议形式化分析与自动化验证领域。主要从逻辑方法、模型检测方法和证明方法3个方面对符号化的安全协议形式化分析方法进行了综述,并指出了今后该领域的研究方向。     

系统芯片的混合验证方法

阐述系统芯片 (SOC)的设计验证特点。综述目前流行的验证方法 ,指出所存在的问题。论述了形式化验证方法和半形式化验证方法的发展状况及新的发展方向和趋势     

形式化方法和混合系统

形式化方法的主要研究对象是计算机系统的设计和验证。这里的计算机系统可以是硬件系统,软件系统,嵌入式系统（ＥｍｂｅｄｄｅｄＳｙｓｔｅｍ）、分布式系统（ＤｉｓｔｒｉｂｕｔｅｄＳｙｓｔｅｍ）、反应式系统（ＲｅａｃｔｉｖｅＳｙｓｔｅｍ）、实时系统（Ｒｅａｌ－ｔｉｍｅｓｙｓｔｅｍ）。近年来,形式化方法的研究领域扩展到混合系统。本文论述形式化方法在混合系统研究中的作用、混合系统的研究内容和意义。重点是评述混合系统的验证方法,并提出混合系统验证研究的途径。     

硬件安全门级细粒度形式化验证方法

针对硬件设计长期缺乏有效的安全验证方法问题,提出了一种硬件安全门级细粒度形式化验证方法．该方法使用形式化语言在逻辑门层面上描述硬件电路的安全属性,构造包含安全属性跟踪逻辑的形式化语义语句,从而将硬件设计转化为电路语义模型,并结合霍尔逻辑三元组理论构造用于验证该模型安全属性的定理．定理的证明过程是以人机交互的方式在定理证明器环境下验证定理的合理性．实验结果表明,该方法能够形式化地遍历电路语义模型的状态空间,精确验证不同输入状态下电路语义模型的安全性．该方法通过构造安全属性跟踪逻辑提高了验证的精确性,结合定理证明提高了验证覆盖率,能够有效地验证硬件设计的安全性．     

形式化技术及其工业应用：现状与展望

近些年来，形式化技术的工业应用得到了长足的发展，并愈来愈引导卢研究人员的关注。形式化技术的成功应用归咨于：便于理解和描述的严格、可视规格语言的建立；可用于系统分析、验证的自动或半自动验证工具的开发。形式化技术的工业应用不仅可以增强所开发系统的可靠度，而且可提高系统开发的效率、同时节省系统开发成本。本文对形式化技术及其工业应用的现状进行了综述，并对该领域的未来研究进行了若干展望。     

投影时序逻辑的公理系统与形式验证

为了采用定理证明的方法对并发及交互式系统进行验证,提出了一阶投影时序逻辑的公理系统．利用投影时序逻辑既可描述待验证系统性质和规范,又可描述其实现模型的特点,在同一投影时序逻辑框架可以方便地对待验证系统进行建模和性质描述,并使用公理系统完成系统性质的证明．最后通过一个实例来展示投影时序逻辑及公理系统在系统验证中的应用．     

概率论在Isabelle/HOL中的形式化

基于测度论在Isabelle/HOL/Isar中形式化了概率论,给出了概率空间在Isabelle/HOL中的形式化定义,形式化验证了概率测度的主要性质。形式化验证了测度扩张定理,为在Isabelle/HOL中构造各种概率空间、形式化验证概率算法和概率系统奠定了基础。     

基于Uppaal的移动IPv6协议的模型检测

采用形式化方法对移动IPv6协议系统建立了时间自动机模型,使用实时模型检测工具Uppaal对所建模型的关键性质：活性、移动性和平滑切换等进行了分析和检测. 检测结果证明,移动IPv6协议在切换时存在丢包现象. 通过分析丢包产生的原因,提出了移动IPv6实现平滑切换的理想时间约束条件,并在理想条件下重新验证了协议的性质. 结合模型在理想约束条件下的检测结果指出了提高移动IPv6移动性能的设想.     

构件式体系结构模型转换的语义一致性

基于软件体系结构模型的形式化描述,从结构语义、公理语义和行为语义等几个方面分析了模型转换中特性保持问题的描述,并建立了相应的判定标准,同时探讨了证明一个转换是否满足某些特性保持约束的方法。这些方法支持以定理证明的方式,对模型转换的语义特性保持进行验证,克服了模型检测的不足。该研究可用于指导模型转换规则的定义和模型映射关系的正确性的验证。     

UML statechart based rigorous modeling of real-time system

Rigorous modeling could ensure correctness and could verify a reduced cost in embedded real-time system development for models. Software methods are needed for rigorous modeling of embedded real-time systems. PVS is a formal method with precise syntax and semantics defined. System modeled by PVS specification could be verified by tools. Combining the widely used UML with PVS, this paper provides a novel modeling and verification approach for embedded real-time systems. In this approach, we provide 1 ) a time-extended UML statechart for modeling dynamic behavior of an embedded real-time system ; 2) an approach to capture timed automata based semantics from a timed statechart; and 3 ) an algorithm to generate a finite state model expressed in PVS specification for model checking. The benefits of our approach include flexibility and user friendliness in modeling, extendability in formalization and verification content, and better performance. Time constraints are modeled and verified and is a highlight of this paper.     

MSVL程序的自动定理证明方法

The MSVL is a temporal logic programming language. It can be used to verify C, Verilog/VHDL programs. To do so, a program written in C or Verilog/VHDL is translated to an MSVL program, and then the task is changed to verify MSVL programs. However, at present, the correctness of MSVL programs can only be proved by hand with deductive approaches. This is tedious and error-prone. To handle this problem, an automatic theorem proving technique for the MSVL based on the interactive theorem prover PVS is proposed. To this end, first the syntax and semantics of the MSVL are described in the specification language of PVS, which enables MSVL programs to be correctly recognized by PVS. Further, an axiomatic system of the MSVL and some theorems are specified. Then the proof commands of PVS are input for invoking the PVS prover to deduce MSVL programs. During verification, simple details can be proved by PVS automatically while complex steps are controlled by human. In this way, MSVL programs can be verified semi-automatically, which facilitates the deduction of MSVL programs. An instance of the bakery algorithm is given to show that our method is feasible.     

Integrating object-oriented methods and formal methods for requirement engineering

High quality software requirement specification is crucial for a software development. Although much efforts and research works have been done to address the problem, the errors in user requirement are still prevent us from developing high quality software. To address the problem, this paper proposes integrating graphical specification technique UML with formal specification technique to construct user requirement specification. We also present a prototype tool to perform the automatic translation from UML specification into Object-Z specification.     

一种结合UML和B的软件需求获取方法

精确的软件需求是软件质量的保证,UML在软件需求中起着重要的作用,它用于描述软件的需求模型、对象模型、动态模型和部署模型.然而UML缺乏形式化方法的准确语义,很难产生准确无歧义的软件规约.使用B和UML结合的方法,借助形式化方法的精确语义和规约级证明义务来产生准确一致的系统规约,并结合家庭智能控制系统说明了结合使用B和UML规约的过程.     

基于构造类别代数的数据流和控制流相结合的协议测试

如何从协议规范中生成即考虑控制流又兼顾数据流的测试用例是一个很有挑战的问题, 本文提出了一种基于构造类别代数的数据流与控制流相结合的测试方法, 给出了在其上的测试用例生成算法, 有限状态机模型到构造类别代数模型的转换算法, 并且给出了在一个实际的路由协议RIP 的测试中的应用例子.     

可视化部件规格匹配的研究

分析了现有的重用部件的检索及匹配方法,提出了一种可视化重用部件的形式化规格描述,讨论了几种基于规格描述的部件匹配,并阐述了不同种类的部件匹配情况下部件的重用方式（黑盒重用或白盒重用）．     

基于时态逻辑的形式化联邦校核方法

提出了一种基于时态逻辑的形式化联邦校核方法，采用时态逻辑公式描述联邦各成员的行为逻辑关系，推导出与该时态逻辑公式对应的有限自动机模型，即规范自动机。同时，建立联邦全局行为的状态转移图，即实现自动机，通过检验规范自动机所接受的语言是否包含实现自动机所接受的语言来判断联邦运行时各成员的状态变化是否满足规范要求，达到校核联邦的目的。该方法可用来校核联邦及其成员的交互设计和逻辑行为运行的正确性和逻辑性，具有理论意义和应用价值。     

概率可靠多播协议Bimodal Multicast的IOA形式规范

介绍并讨论了Bimodal Multicast的应用特征和规范形式描述方法,给出了一个基于I/O自动机的描述方案,内容包括Bimodal Multicast中消息的表达,状态和动作的定义,并重点讨论了Bimodal Multicast的最近最先语义的描述方法.     

立法伦理的向度及其实现

立法伦理作为对法之创制活动的应然性规定,具有从＂源头＂上确保法治成为善治的重要意义。在向度上,立法伦理表现为所立之法应该符合形式合理性和实质合理性两个要件。而通过法之创制使价值形态的道德内蕴于法律之中,将一定的规范形态的道德转换为法律规范,则是立法伦理实现的两个方面。