精华内容
下载资源
问答
  • 形式化规范在软件可靠性研究中能够起到的作用是多方面的。本文针对非形式化统计使用测试的不足,结合已有的早期可靠性估计方法,设计了优化算法,并提出了即使在设计中采用了形式化规范仍然需要测试的结论。
  • 基于服务的软件形式化规范的进化方法
  • 本文介绍了我们在几何知识对象的识别,形式化,结构化和规范化方面的工作,目的是进行语义表示和知识管理。 我们根据几何知识在几何文献中的积累和表示方式对几何知识进行分类,通过调整一阶逻辑的语言来对几何知识...
  • 使用形式化方法规范列车控制系统
  • 北大裘宗燕老师的《Z语言形式化方法》,Z语言用于编写软件规范,严格的指导编码过程。
  • 形式化方法一般可分为形式化规范说明Formal Specification,和形式化验证Formal Verification。 Formal Formal Specification 形式化规范说明 Formal Verification 形式化验证 Theorem Proving 定理检测/Deductive...

    【1】 概述

    硬件和软件系统在规模和功能上的增长增加了复杂性,也 增加了潜在错误的可能性,这些错误引起了金钱、时间上的损 失,甚至会危及人们的生命。形式方法是用于软件和硬件系统 的规范,开发和验证的特定类型的基于数学的技术,是改善和 确保系统质量的重要方法。形式化方法在软件和硬件领域中 的应用进展比较显著,引起了各个领域的注意[1]。形式化验证 方法是形式化方法的一个重要的研究内容,本文主要对形式化 验证方法进行探讨。

    形式化方法一般可分为形式化规范说明Formal Specification,和形式化验证Formal Verification。

    Formal

    • Formal Specification 形式化规范说明
    • Formal Verification 形式化验证
      • Theorem Proving 定理检测(证明)/Deductive Verification 演绎检测
      • Model Checking 模型检测
      • Automated Test Case Generation 自动测试用例生成

    在这里插入图片描述

    【2】基本概念

    【2.1】形式化规范说明

    硬件和软件系统在规模和功能上的增长增加了复杂性,也 增加了潜在错误的可能性,这些错误引起了金钱、时间上的损 失,甚至会危及人们的生命。形式方法是用于软件和硬件系统 的规范,开发和验证的特定类型的基于数学的技术,是改善和 确保系统质量的重要方法。形式化方法在软件和硬件领域中 的应用进展比较显著,引起了各个领域的注意[1]。形式化验证 方法是形式化方法的一个重要的研究内容,本文主要对形式化 验证方法进行探讨。

    【2.2】形式化验证

    【2.2.1】定理证明

    定理证明:先对系统及其性质进行抽取,表示成基于某种 逻辑的命题、谓词、定理,在验证者的引导下,不断地对公理、以 证明的定理施加推理规则,产生新的定理,直到推导出表达系 统性质的公式,从而证明设计的系统满足该性质。现在定理证 明器越来越多的应用在验证硬件和软件设计的安全临界性质 的验证[3]。 定理证明高度抽象,具有强大的逻辑表达能力,可以验证 几乎所有的系统行为特性,可以处理无限的状态空间。定理证 明器可以分为三种:自动定理证明器、交互式定理证明器及证 明检验器。现在大多数定理证明器是交互式的,需要人的引 导,对验证者的要求有良好的数学经验。 主要的定理证明工具有:STeP(Stanford)、TLV、AL2(UTAus⁃ tin/CLI)、Coq、HOL(Cambridge)、Isabelle(Cambridge)、Larch、Nu⁃ prl、PVS(SRI)等。

    【2.2.2】模型检测

    模型检测是一种通过对目标系统建立一个有限的模型,并在模型发生改变时,检测希望满足的性质,例如安全性和活性在该模型中是否成立、稳定的技术。

    目前有两种主要模型检测技术:

    • 一种是时态模型检测,这 种方法中规范说明用时态逻辑公式表示,系统用有限状态转换模型表示,用模型检测器检测模型是否满足规范说明公式。
    • 另外一种是等价性检测,这种方法中规范说明用一个自动机表示,系统用一个自动机表示,然后证明两个模型是否一致。

    自动化程度较高是模型检测的优点,并且当系统不满足给 定的性质时,可以给出反例,使设计人员方便找出设计错误。 模型检测应用于硬件和协议的验证,现在在对软件设计的验证 已成为研究的热点。状态空间爆炸问题是其主要的缺点。

    主要的模型检测工具有:

    • COSPAN/FORMALCHECK(Bell)、
    • MURPHY(Stanford)、SPIN(Bell)、
    • SMV(CMU)、
    • VIS(Berkeley)等。

    目前形式化验证方法成功应用于商业、航空业、通信业和 芯片制造业,INTEL,ARM和NIVIDA等大公司已经把形式化方法应用到芯片的制造和验证[5]。

    从本质上讲,模型检测技术就是穷尽对状态空间的搜索,并通过模型的有限性来保证该搜索过程一定会终止。最初的模型检测应用在硬件和协议验证领域,十分成功,后来在软件系统的验证上也得到了广泛应用。

    Reference:

    [形式化验证方法浅析] 陈波1,李夫明2 (1.山东理工大 学 计算机科学与技术学院,山东 淄博255000; 2.山东理工大学 数学与统计学院,山东 淄博255000)**

    后续待阅读资料

    线性时序逻辑 https://www.docin.com/p-506137477.html
    模型检测 https://wenku.baidu.com/view/800eade45a8102d277a22f3a.html?fr=search
    model checking overview and buchi automata and LTL https://www.docin.com/p-1003260979.html

    展开全文
  • 形式化验证调研报告

    千次阅读 2018-10-17 14:56:24
    形式化验证调研报告 王立敏 中国科学院信息工程研究所 第五实验室 北京 中国100093 摘要2018年初,Spectre和Meltdown漏洞的发现,使得芯片安全备受重视。然而传统的基于仿真的芯片验证方法由于测试样例覆盖不完全...
    形式化验证调研报告
    王立敏
    中国科学院信息工程研究所 第五实验室 北京 中国100093

    摘要2018年初,Spectre和Meltdown漏洞的发现,使得芯片安全备受重视。然而传统的基于仿真的芯片验证方法由于测试样例覆盖不完全,验证过程耗时巨大,逐渐适应不了日益复杂的芯片了。形式化方法作为一种静态验证方法,正好可以解决这些问题。本文主要梳理了当前形式化方法检测的常见方法,并且列出他们的优缺点,以及前人对这些缺点的改良方法。

    关键词
    芯片安全,形式化验证,二元决策图,时序逻辑,Petri网,定理证明,等效性检验,模型检验

    Formal Verification Investigation Report
    Wang Liming 1
    Institute of Information Engineering, Chinese Academy of Sciences, Beijing 100093, China

    Abstract At the beginning of 2018, the discovery of Spectre and Meltdown attacks made chip security receive much more concerns. However, due to the serious drawbacks in the simulation-based methods in tradition such as the test cases did not cover all of the inputs and the time consuming of the simulation, this method became inappropriate to validate the chips that became more and more complicated. Formal Methods is a static verification method, which would solve these problems that the simulation-based methods bright. This report would list their advantages and disadvantages, as well as the previous methods that attempt to solve these problems.

    Key words Chip security, Formal verification, Binary Decision Diagrams,Temporal logic, Petri net, Theorem Proving, Equivalence Checking, Model checking

    1 引言

            近些年来,芯片的性能和规模不断提升,集成电路的设计也越来越复杂,使得引入错误和问题的可能性日益增加。但是传统的基于仿真的集成电路验证方法的覆盖率难以达到100%。而形式化方法作为一种静态测试的方法,通过数学的推理证明,理论上可以实现绝对安全,找出难以发现的错误,因此广受研究人员的关注。

    基于仿真的集成电路验证

            目前应用最广泛的依然是基于仿真的验证方法。这种验证方法通常需要一个测试基准,通常同时对待验证的电路和测试基准施加相同的激励,然后通过对比他们的输出来判断电路是否正确。这些输入向量可以事先生成,然后在测试期间从数据库读入,也可以边测试边生成。

            基于仿真的验证只能证明电路在指定的输入向量下输出正确,若要证明电路的正确性,输入向量必须覆盖电路的所有输入组合。但是现在集成电路十分复杂,要实现这一点是十分困难的。令人遗憾的是,许多不安全的因素或者错误都是出现在测试向量难以覆盖的地方[1]。而且这种验证方式主要用于发现逻辑漏洞,而并不能检查出芯片中的安全漏洞。

    基于形式化方法的验证

            基于形式化方法的验证是通过数理逻辑推理的一种方法。一般分为形式等效性检验(Equivalence
    Checking),定理证明(Theorem Proving)以及模型检查(Model
    Checking),如图1所示。

    图1 形式化方法的分类

    图1 形式化方法的分类

            形式等效性检验一般用于检测两个电路设计逻辑相等,电路设计一般使用硬件描述语言(Verilog或者VHDL)进行描述,然后综合成门级电路,接着再进行一系列的优化。这里的每一个步骤都会导致电路设计的改变,因此检查每一步操作前后的电路设计是否逻辑等效是有必要的。有些时候优化操作需要人为干预,因此也需要使用等效性检验来确保这些操作没有引入错误。除此之外,设计完成的芯片也需要与对应的黄金模型进行对比,以确保集成电路设计的正确性。

            定理证明方法是一种将模型抽象为逻辑公式,然后使用自动的逻辑推理技术来验证电路是否正确的技术。但是定理证明方法在使用时需要专业人士事先制定大量的定理和推理策略。因此它在自动化推理方面能力较差,不适用大规模的系统。

            模型检验是一种基于状态迁移系统的自动验证技术。它最早是由Edmund M.
    Clarke和他的研究生E.A. Emerson以及A.P.Sistla提出来的[2]。使用这种方法首先需要提出一系列规格属性,这些属性表示对电路的安全需求,系统只要满足这些属性,就能确保安全。然后建立一个电路系统的模型,即可通过模型检测方法自动地检测模型是否满足这些规格属性。模型检验一般用于电路和协议的验证。

    总结

            基于仿真的集成电路验证需要输入向量,而形式化验证并不需要。前者是先生成输入向量,再验证输出向量,而后者的考虑方向则相反,要先指明什么样的输出是符合要求的,再利用形式化方法去证明它。由于基于仿真的集成电路验证存在覆盖率不能达到100%,以及仿真时间过长等问题,而形式化证明则正好能解决这些问题。因此形式化验证开始被研究人员广泛关注。

    模型的建立

            要使用形式化方法,需要先为电路建立模型,这些模型通常用一些图的数据结构或者公式来表示。形式化模型建立完成后,即可使用形式化算法对其进行检验。

    二元决策图
    2.1.1 二元决策图概述

            二元决策图(Binary Decision Diagrams,BDD)可以很好地表示一个布尔函数。所谓布尔函数,即定义域和值域都是布尔值的函数,布尔函数在电路设计和密码学方面有广泛的应用。由于电路的输入和输出都是二进制值,这意味着电路可以表示成一个布尔函数,因此使用BDD结构来表示电路是十分合适的。

    2.1.2一个例子

    表1 f(x1,x2,x3)的真值表

    x1x2x3f(x1,x2,x3)
    0000
    0010
    0100
    0111
    1001
    1010
    1100
    1111

            假设有一个电路,电路的功能如公式(1)所示。
    (1) f ( x 1 , x 2 , x 3 ) = x 1 x 2 + x 1 x 2 ‾ x 3 ‾ f(x1,x2,x3)=x1x2+x1\overline{x2}\overline{x3} \tag{1} f(x1,x2,x3)=x1x2+x1x2x3(1)

            其真值表如表1所示。于是可得出该电路的BDD图,如图2,x1,x2,x3为变量,实线表示变量赋值为1,虚线表示变量赋值为0。

            由表1真值表可得,当x1,x2,x3分别赋值为0时,f(x1,x2,x3)的值也为0。则如图2在BDD图中沿着x1,x2,x3,0之间的虚线最终也会到达0的地方。如图中所示这样变量有序的BDD图也可以称作有序二元决策图(Ordered Binary Decision Diagrams ,OBDD)图。

            可以发现,当x1赋值为0,x2也赋值为0时,无论x3赋何值,最终结果也是0,因此可以将BDD再做精简。如图3中简化后的BDD所示,可以将这条路径中的x3节点删除,直接将x2用虚线连接至0处,这个过程可称为BDD的简化,而最终的简化结果则称为简化的有序二元决策图(Reduced
    Ordered Binary Decision Diagrams,ROBDD)。

    图2 f(x1,x2,x3)的BDD图

    图2 f(x1,x2,x3)的BDD图

    图3 f(x1,x2,x3)的简化BDD图

    图3 f(x1,x2,x3)的简化BDD图
    2.1.3基于二元决策图的电路表示

            对于组合逻辑电路而言,可以直接使用上述方法生成BDD结构。但是对于时序逻辑电路而言,则需要根据其特点生成有限自动机(Finite State Machine,FSM),再使用BDD来表示FSM的状态变迁过程,在形式等效验证和符号模型检验中常采用这一方法来表示电路。

            BDD本身不能减少状态空间,随着变量数的增加,状态空间数依然呈指数级上涨,但是它也有许多优点,比如表达形式简洁,并且配合图算法可实现快速的操作,用于表示电路十分合适。

    时序逻辑

            时序逻辑是逻辑领域中一个重要的组成部分,它在形式化验证中有十分重要的应用

    表2 时序逻辑的操作

    符号操作解释
    θUψUntil若θUψ在路径上为真,则θ一直保持真直到ψ为真
    θRψRelease若ψ为真,直到θ为真(或者θ永远不为真)则θRψ在路径上为真,
    Next若Xθ在路径上为真,则下一个时刻θ为真
    Future若Fθ在路径上为真,则θ最终一定为真
    Globally若Gθ在路径上为真,则任何时刻,θ都为真
    All表示对于任意路径
    Exists表示存在这样的路径

            可以使用如表2所示的符号来描述硬件系统的行为,例如我们要表示“信号A一直不变,直到上升沿才翻转”这一操作,则我们令p为“信号A不变”,q为“时钟到达上升沿”,则该操作可表示为当满足pUq使信号A翻转。

            比较常用的时序逻辑是线性时序逻辑(Linear temporal logic,LTL)以及计算树逻辑(Computation tree logic,CTL)。线性时序逻辑是个线性结构,每一个时刻都只对应一个后继,计算树逻辑则是一个树状的分支结构。LTL可用于重点对象的分析,并且它可以使用公平的概念,但是对于一些可返回到初始状态的复杂系统,LTL则无法表示。CTL则相反,它无法使用公平的概念,但是却可以表达一些较为复杂的系统[3]。LTL和CTL各有自己的优势,E. A. Emerson 和 Joseph Y. Halpern 在 1986年提出了CTL*,统一了LTL和CTL。在传统的模型检验中,通常采用时序逻辑来描述电路。

    Petri网

            Petri网是一种重要的数学工具,Petri网对系统的并发性,异步性和不确定性具有很强的描述能力,一般主要是使用Petri网的可达图[4]。

    Petri网通常为四元组N= <P,T,F,M0>

    P:库所(Place)的有限集

    T:迁移(Transition)的有限集

    F:F ⊆ (P x T) ∪ (T x P),表示边的集合。∪前后分别表示输入函数集以及输出函数集。

    M0:P->N,表示初始状态集

    库所(Place)表示系统的状态。一般用圈圈表示。

    迁移(Transition)则表示资源的消耗使用,一般用黑色矩形表示。

            连接库所与变迁的有向弧表示输入输出函数。用令牌Token表示库所中的资源数量,一般用●表示。

            资源会沿着有向弧流动,当资源足够时,便会触发某些操作的执行来使用和消耗资源。即令牌会不断沿着迁移流动,令牌在迁移之前积聚叫做迁移的使能(enabled),令牌积累到足够数量之后便能通过迁移,这一过程也叫迁移的激发(fire)。

            图4表示一个互斥系统的Petri网,双方发出进入临界区的请求,当其中一方进入临界区时,另一方只能等待。图中的小黑点表示Token,最中间的库所t表示哪一方可优先访问临界区,当Idle中的Token传递到Wait时,t中个Token也会流到可优先进入临界区的那一方,于是便可以激发迁移Access,当经过Free之后,Token又将回到Idle和t中。

    图4 互斥模型的Petri网

    图4 互斥模型的Petri网

    1.形式化方法

    形式等效验证(Equivalence Checking)

            假设我们有Spec1和Spec2两个模型。若需要验证综合优化前后两个模型是否逻辑相等,则Spec1和Spec2可分别表示综合优化前后的设计。若需要验证设计的正确性,Spec1通常为黄金模型,Spec2则为我们的设计。Spec1和Spec2通常使用相同的数据结构,例如BDD,再根据具体的需求使用诸如布尔SAT求解程序(求解可满足性问题)之类的算法来进行等效性检验。

            虽然等效检验的检测效果不错,在工业上也得到了应用,但是在使用过程中依然需要高层次的专业人员去制定等效检验框架[5]。而且在复杂的电路中,等效性检验也存在状态空间数呈指数级增长的问题。虽然学术界提出了各种优化的方法,比如将复杂的等效检验切割成小的可比较集合进行处理[6],或者利用算法优化减少空间消耗[7],但是状态空间爆炸问题依然没有很好地解决。

    定理证明(Theorem Proving)

            定理证明方法十分严格,跟数理逻辑结合十分紧密。一般使用高阶逻辑(Higher-Order
    Logic,HOL) 系统来进行证明。

            要验证一个大的系统,通常采用目标制导的方式。将系统用HOL表示出来之后,再分为若干个子命题分别证明。定理证明方法对硬件模块的验证一般会用到抽象技术和层次化验证技术

            在证明之前需要对系统进行建模,Mike Gordon在论文[8]中提出可以直接利用HOL来为硬件建模。一个器件模块只有输入输出,这些输入输出可以用HOL中的谓词和函数表示,而模块之间的连接可用合取表示。

            抽象技术主要用于将系统的详细信息掩盖掉,只考虑需要关注的性质,这样可以方便算法的处理。根据关注对象的不同,可以分为不同的抽象。例如结构抽象掩盖了内部结构信息而只描述了设备的规范,而行为抽象则只对模块的部分行为进行定义,数据抽象则是通过一个映射,将现实中的数据抽象为一个较小的抽象数据集,比如布尔真值。

            层次化验证技术是将大的模型划分为小的模型,构建成一个树状结构,每一个子节点都是父节点的细化。下一层的正确性可以证明上一层的正确性,因此自下而上地证明可以确保根节点的模型的正确性。

            定理证明方法在工业上也有一定的使用,但是定理证明方法需要对系统用严格语义的数学符号进行描述和推理,因此对用户而言十分复杂。而且并没有办法确保事先人为制定的规则和定理的正确性,因此最终的正确性也值得怀疑,即前提若有错误,则最终的验证结果就不一定正确。

    模型检验(Model Checking)

            模型检验是目前最为流行的形式化检测方法。但是它依然存在状态空间爆炸的问题,模型检测方法的发展几乎都是为了解决状态空间爆炸问题以及不同系统的适用性问题展开的。

            状态空间爆炸问题一直制约着模型检验方法的发展,为此科研人员一直寻找合适的方法来解决这一问题,例如符号模型检验,偏序规约技术,以及近些年来十分热门的SAT技术。

    3.2.1符号模型检验

            符号模型检验的提出是解决状态空间爆炸问题的一个里程碑,它采用OBDD来描述电路。这使得模型检验可检查的系统规模大大增加,可以超过1020个状态。

            McMillan最先将OBDD引入模型检验技术[9],提出了符号模型检验,最初时符号模型检验只是基于CTL公式的。该方法将CTL公式转化成OBDD图,并在OBDD上搜索状态空间。之后Clarke等人又提出了基于LTL的符号模型[10]。

            符号模型检验中,存在许多优化方法,最常见的两种方法是偏序规约技术[11]和抽象模型[12]。

            由于系统中可能存在两个并行的模块,而这些并行模块的运行组合有许多种,其中的一部分运行组合实际上是重复的。因此若能将并行的模块的运行次序固定下来,在验证过程中就可以减少许多重复的路径。

            抽象技术多用于需要数据处理的系统,符号模型检验的数据处理能力较弱,若是需要表达复杂的数据结构,则验证的复杂性会十分的高。因此可以将精确的数据值和抽象的数据集合做个映射,产生一个较小的抽象数据集,以此来简化符号模型检验的状态空间。

    3.2.1 SAT技术

            基于BDD的符号模型检验虽然使得可检验的系统规模增加了许多,但是状态空间爆炸问题并没有彻底解决,在BDD中,状态空间依然是指数级增长的。BDD可通过简化生成ROBDD来减少状态空间,但是可优化的余地依然比较少。随着SAT技术的发展,它也被引入到模型检验领域[13]。

            SAT是NP完全的方法,因此它也是指数爆炸型的,为此Clarke等人提出了限界模型检验[14]。模型检验是通过对整个系统建模,并证明我们的模型是否满足我们定义的属性规格。而限界模型检验,则通过广度搜索的方法,从长度为1的路径开始搜索,搜索的路径长度逐渐递增,若能在长度为K的路径中搜索到不符合属性规格的路径,则停止搜索并报告这一反例。

            虽然限界模型检验搜索到反例后即可停止这一机制使得其遍历的状态大大减少,但是它只检查了整个状态空间的一个子集,只能证明在限界中的那部分状态符合属性规格,而无法证明整个状态空间符合属性规格。

            为了解决这一完整性问题,目前学术界较为流行的做法是逼近所求的解,即迭代地计算可达状态的不动点,来验证这整个模型是否最终满足规约。

            Yakir Vizel等人于2015年整理了各种适用于SAT的优秀的算法,这些算法包括冲突驱动从句学习(Conflict-Driven
    Clause Learning),随机局部搜索(Stochastic Local Search)[15]。

            SAT技术在经过EDA社区与科研人员的相互促进之下,在过去十年中取得了很大的进步。虽然SAT在工业界也得到了应用,但是它依然无法很好地解决模型检验的状态空间爆炸问题和限界模型检验的完整性问题,此外并行SAT技术也是一个十分有前景的方向。

            而为了解决不同系统的适应性问题,如第2部分所述,研究人员提出了许多不同的建模方式。传统的模型检验方法一般采用时序逻辑来描述电路。

    4 讨论

            传统的基于仿真的验证方式虽然存在有覆盖不完全,耗时间等问题。而形式化验证则正好可以解决这些问题,然而这并不意味着形式化方法可以完全替代传统的仿真验证。形式化方法依然存在许多的局限性,目前最好的办法是将传统的仿真验证与形式化验证结合起来。

            虽然在工业界和学术界的共同促进之下,形式化验证技术有了长足的进步。但依然存在不少进步的空间。模型验证是目前自动化水平最优的,很少需要手动干预,但是状态空间爆炸的问题依然令人十分困扰。为了提高形式化验证的速度,研究人员依然在尝试攻克检测技术的并行化的问题,这也是目前较为火的一个方向。此外为了能够使用到工业界,形式化验证必然还是需要提高检测技术的自动化水平,例如门级信息流的方法[16]利用关键信息只能从低安全级流向高安全级这一特性,简化了形式化方法建模的流程,使其可以自动生成模型。此外,纵观整个形式化验证方法的发展历程,可以发现许多形式化验证的突破,都是因为将一些已经存在的理论成果移植应用到工程中去,因此我们也可以从这一方面去考虑如何改进形式化验证的方法。

            形式化方法是个十分有前景而又十分重要的研究方向,不仅可以用于检测出难以发现的逻辑错误,也可以检查电路中隐藏的硬件木马,甚至发现较为隐秘安全漏洞。因此上述的一些形式化方法的局限依然值得我们在日后重点研究。

    参考文献

    [1] LAM W K. Hardware Design Verification: Simulation and Formal Method-Based
    Approaches (Prentice Hall Modern Semiconductor Design Series)[M]. Upper Saddle
    River, NJ, USA: Prentice Hall PTR, 2005.

    [2] CLARKE E M, EMERSON E A. Design and synthesis of synchronization skeletons
    using branching time temporal logic[J]. : 20.

    [3] 张瑞雪, 郝春梅, 王旭. 计算机形式验证方法研究综述[J]. 中国电子商务, 2011(5):
    69–69.

    [4] 蒋屹新, 林闯, 邢栩嘉. 基于线性时态逻辑的Petri网模型检测[J]. 系统仿真学报,
    2003, 15(z1): 6–10.

    [5] KREIKER J, TARLECKI A, VARDI M Y等. Modeling, Analysis, and Verification -
    The Formal Methods Manifesto 2010 (Dagstuhl Perspectives Workshop 10482)[J].
    HERBSTRITT M. 2011.

    [6] KUEHLMANN A, KROHM F. Equivalence Checking Using Cuts and Heaps[J]. : 6.

    [7] PARUTHI V, KUEHLMANN A. Equivalence checking combining a structural
    SAT-solver, BDDs, and simulation[C]//IEEE Comput. Soc, 2000: 459–464.

    [8] HAN J, STONE G. The implementation and verification of a conditional sum
    adder[J]. 1988.

    [9] MCMILLAN K L. Symbolic checking,An approachto the state explosion
    problem[J]. : 212.

    [10] CLARKE E, GRUMBERG O, HAMAGUCHI K. Another look at LTL model
    checking[C]//International Conference on Computer Aided Verification. Springer,
    1994: 415–427.

    [11] PELED D. All from one, one for all: on model checking using
    representatives[G]//COURCOUBETIS C. Computer Aided Verification. Berlin,
    Heidelberg: Springer Berlin Heidelberg, 1993, 697: 409–423.

    [12] CLARKE E M, GRUMBERG O, LONG D E. Model checking and abstraction[J]. ACM
    transactions on Programming Languages and Systems (TOPLAS), 1994, 16(5):
    1512–1542.

    [13] 王瑞. 基于SAT的符号化模型检验技术研究[D]. 国防科学技术大学, 2014.

    [14] CLARKE E, BIERE A, RAIMI R等. Bounded Model Checking Using Satisfiability
    Solving[J]. : 20.

    [15] VIZEL Y, WEISSENBACHER G, MALIK S. Boolean Satisfiability Solvers and Their
    Applications in Model Checking[J]. Proceedings of the IEEE, 2015, 103(11):
    2021–2035.

    [16] HU W, MAO B, OBERG J等. Detecting Hardware Trojans with Gate-Level
    Information-Flow Tracking[J]. Computer, 2016, 49(8): 44–52.

    Blog:形式化验证调研报告

    展开全文
  • 需求规范错误是软件设计错误的一大类。该文提出了一个软件需求的形式化转换模型,用来将软件需求分析直接、自动地转换为形式化描述,为需求验证提供帮助,避免软件在需求规范上可能产生的错误。
  • 何为规范化、标准、精细管理

    千次阅读 2020-12-22 13:36:32
    一、规范化管理规范化管理就是从企业生产经营系统的整体出发,对各环节输入的各项生产要素、转换过程、产出等制订制度、规程、指标等标准(规范),并严格地实施这些规范,以使企业协调统一地运转。实行规范化管理在...

    一、规范化管理

    规范化管理就是从企业生产经营系统的整体出发,

    对各环节输入的各项生产要素、

    转换过程、产出等制订制度、规程、指标等标准(规范)

    ,并严格地实施这些规

    范,以使企业协调统一地运转。

    实行规范化管理在理论和实践中都证明是极为重要的。

    首先,

    这是现代化大生产

    的客观要求。

    现代企业是具有高度分工与协作的社会化大生产,

    只有进行规范化

    管理,

    才能把成百上千人的意志统一起来,

    形成合力为实现企业的目标而努力工

    作。

    其次,

    实行规范化管理是变人治为法治的必然选择。

    每个员工都有干好本职

    工作的愿望,但在没有

    干好

    的标准的情况下,往往凭领导者的主观印象进行考

    核和奖惩,

    难免出现在管理中时紧时松、

    时宽时严的现象,

    并很容易挫伤员工的

    积极性。

    按照统一的规范进行严格管理,人和人之间可以公正比较、平等竞争。最后,实

    行规范化管理是提高员工总体素质的客观要求。

    规范使员工明确企业对自己的要

    求,

    有了努力的标准,

    必然能逐步提高自己的素质;

    员工还可以对照规范进行自

    我管理。

    因为规范是在系统原则下设计出来的,

    管理人员依据规范进行管理,

    能提高立足本职、纵观全局的管理水平。

    二、标准化管理

    所谓标准,

    是指依据科学技术和实践经验的综合成果,

    在协商的基础上,

    对经济、

    技术和管理等活动中,

    具有多样性的、

    相关性征的重复事物,

    以特定的程序和形

    式颁发的统一规定。标准可分为技术标准和管理标准两大类。

    技术标准是对技术活动中,

    需要统一协调的事物制定的技术准则。

    它是根据

    不同时期的科学技术水平和实践经验,针对具有普遍性和重复出现的技术问题,

    提出的最佳解决方案。

    管理标准是企业为了保证与提高产品质量,

    实现总的质量目标而规定的各方

    面经营管理活动、

    管理业务的具体标准。

    若按发生作用的范围分,

    标准又可分为

    国际标准、国家标准、部颁标准和企业标准。以生产过程的地位分,又有原材料

    标准、零部件标准、工艺和工艺装备标准、产品标准等。在标准化工作中,又通

    常把标准归纳为:基础标准、产品标准、方法标准和卫生安全标准。

    标准化是制度化的最高形式,可运用到生产、开发设计、管理等方面,是一

    种非常有效的工作方法。

    作为一个企业能不能在市场竞争当中取胜,

    决定着企业

    的生死存亡。

    企业的标准化工作能不能在市场竞争当中发挥作用,

    这决定标准化

    在企业中的地位和存在价值。

    展开全文
  • 什么是形式化

    千次阅读 2018-08-10 05:22:32
    形式化方法在古代就运用了,而在现代逻辑中又有了进一步的发展和完善。这种方法特别在数学、计算机科学、人工智能等领域得到广泛运用。它能精确地揭示各种逻辑规律,制定相应...

        形式化方法在古代就运用了,而在现代逻辑中又有了进一步的发展和完善。这种方法特别在数学、计算机科学人工智能等领域得到广泛运用。它能精确地揭示各种逻辑规律,制定相应的逻辑规则,使各种理论体系更加严密。同时也能正确地训练思维、提高思维的抽象能力。形式化方法英文的名称是formal methods。

        形式化方法是基于数学的特种技术,适合于证。将形式化方法用于软件和硬件设计,是期望能够像其它工程学科一样,使用适当的数学分析以提高设计的可靠性和鲁棒性。但是,由于采用形式化方法的成本高意味着它们通常只用于开发注重安全性的高度整合的系统。

        形式化是指分析、研究思维形式结构的方法。它把各种具有不同内容的思维形式(主要是命题和推理)加以比较,找出其中各个部分相互联结的方式,如命题中包含概念彼此间的联结,推理中则是各个命题之间的联结,抽取出它们共同的形式结构;再引入表达形式结构的符号语言,用符号与符号之间的联系表达命题或推理的形式结构。例如,把全称肯定命题,用符号形式化为“SAP”;把联言命题、假言命题分别形式化为:“p∧q、“p→q”。又例如:一个具体的假言联言推理“如果这种金属是纯铝,那么它的物理性质必与纯铝相同;如果这种金属是纯铝,那么它的化学性质必与纯铝相同;但这种金属的物理性质和化学性质与纯铝不相同;所以,它不是纯铝。”这个推理的形式结构是:“如果p,则q;如果p,则r;非q且非r;所以非p。”可进而形式化为下列公式:((p→q)∧(p→r)∧┐q∧┐r→┐p。

     

    640?wx_fmt=jpeg

    形式化方法发展过程

        软件形式化方法最早可追溯到20世纪50年代后期对于程序设计语言编译技术的研究,即J.Backus提出BNF描述Algol60语言的语法,出现了各 种语法分析程序自动生成器以及语法制导的编译方法,使得编译系统的开发从“手工艺制作方式”发展成具有牢固理论基础的系统方法。形式化方法的研究高潮始于 20世纪60年代后期,针对当时所谓“软件危机”,人们提出种种解决方法,归纳起来有两类:一是采用工程方法来组织、管理软件的开发过程;二是深入探讨程 序和程序开发过程的规律,建立严密的理论,以其用来指导软件开发实践。前者导致“软件工程”的出现和发展,后者则推动了形式化方法的深入研究。经过30多 年的研究和应用,如今人们在形式化方法这一领域取得了大量、重要的成果,从早期最简单的形式化方法——一阶谓词演算方法到现在的应用于不同领域、不同阶段 的基于逻辑、状态机、网络、进程代数、代数等众多形式化方法。形式化方法的发展趋势逐渐融入软件开发过程的各个阶段,从需求分析、功能描述(规约)、(体 系结构/算法)设计、编程、测试直至维护。

     

    形式化方法定义

        用于开发计算机系统的形式化方法是描述系统性质的基于数学的技术,这样的形式化方法提供了一个框架,可以在框架中以系统的而不是特别的方式刻划、开发和验 证系统。 如果一个方法有良好的数学基础,那么它就是形式化的,典型地以形式化规约语言给出。这个基础提供一系列精确定义的概念,如:一致性和完整性,以及定义规范 的实现和正确性。 形式化方法的本质是基于数学的方法来描述目标软件系统属性的一种技术。不同的形式化方法的数学基础是不同的,有的以集合论和一阶谓词演算为基础(如Z和 VDM),有的则以时态逻辑为基础。形式化方法需要形式化规约说明语言的支持。

     

    形式化方法研究内容

        形式化方法的一个重要研究内容是形式规约(Formal Specification,也称形式规范或形式化描述),它是对程序“做什么”(what to do)的数学描述,是用具有精确语义的形式语言书写的程序功能描述,它是设计和编制程序的出发点,也是验证程序是否正确的依据。对形式规约通常要讨论其一 致性(自身无矛盾)和完备性(是否完全、无遗漏地刻画所要描述的对象)等性质。形式规约的方法主要可分为两类:一类是面向模型的方法也称为系统建模,该方 法通过构造系统的计算模型来刻画系统的不同行为特征;另一类是面向性质的方法也称为性质描述,该方法通过定义系统必须满足的一些性质来描述一个系统。不同 的形式规约方法要求不同的形式规约语言,即用于书写形式规约的语言(也称形式化描述语言),如代数语言OBJ、Clear、ASL、ACT One/Two等;进程代数语言CSP、CCS、π演算等;时序逻辑语言PLTL、CTL、XYZ/E、UNITY、TLA等;这些规约语言由于基于不同 的数学理论及规约方法,因而也千差万别,但它们有一个共同的特点,即每种规约语言均由基本成分和构造成分两部分构成。前者用来描述基本(原子)规约,后者 把基本部分组合成大规约。构造成分是形式规约研究和设计的重点,也是衡量规约语言优劣的主要依据。

        形式验证形式化方法的另一重要研究内容是形式验证(Formal Verification)。形式验证与形式规约之间具有紧密的联系,形式验证就是验证已有的程序(系统)P,是否满足其规约(φ,ψ)的要求(即P (φ,ψ)),它也是形式化方法所要解决的核心问题。传统的验证方法包括模拟(simulation)和测试(testing),它们都是通过实验的方法 对系统进行查错。模拟和测试分别在系统抽象模型和实际系统上进行,一般的方法是在系统的某点给予输入,观察在另一点的输出,这些方法花费很大,而且由于实 验所能涵盖的系统行为有限,很难找出所有潜在的错误。基于此,早期的形式验证主要研究如何使用数学方法,严格证明一个程序的正确性(即程序验证)。

     

    形式化方法分类

        根据说明目标软件系统的方式,形式化方法可以分为两类:

        1)面向模型的形式化方法。面向模型的方法通过构造一个数学模型来说明系统的行为。

        2)面向属性的形式化方法。面向属性的方法通过描述目标软件系统的各种属性来间接定义系统行为。

        根据表达能力,形式化方法可以分为五类:

        1)基于模型的方法:通过明确定义状态和操作来建立一个系统模型(使系统从一个状态转换到另一个状态)。用这种方法虽可以表示非功能性需求(诸如时间需求),但不能很好地表示并发性。如:Z语言,VDM,B方法等。

        2)基于逻辑的方法:用逻辑描述系统预期的性能,包括底层规约、时序和可能性行为。采用与所选逻辑相关的公理系统证明系统具有预期的性能。用具体的编程构 造扩充逻辑从而得到一种广谱形式化方法,通过保持正确性的细化步骤集来开发系统。如:ITL(区间时序逻辑),区段演算(DC),hoare 逻辑,WP演算,模态逻辑,时序逻辑,TAM(时序代理模型),RTTL(实时时序逻辑)等。

        3)代数方法:通过将未定义状态下不同的操作行为相联系,给出操作的显式定义。与基于模型的方法相同的是,没有给出并发的显式表示。如:OBJ, Larch族代数规约语言等;

        4)进程代数方法:通过限制所有容许的可观察的过程间通信来表示系统行为。此类方法允许并发过程的显式表示。如:通信顺序过程(CSP),通信系统演算 (CCS),通信过程代数(ACP),时序排序规约语言(LOTOS),计时CSP(TCSP),通信系统计时可能性演算(TPCCS)等。

        5)基于网络的方法:由于图形化表示法易于理解,而且非专业人员能够使用,因此是一种通用的系统确定表示法。该方法采用具有形式语义的图形语言,为系统开发和再工程带来特殊的好处。如 Petri图,计时Petri图,状态图等。

    640?wx_fmt=jpeg

    展开全文
  • 形式化方法(一) 逻辑部分概念梳理

    千次阅读 2015-12-08 10:59:59
    逻辑部分概念梳理Logic 逻辑 ...逻辑是一门规范性的科学 deals with what entails or what follows from what 解决两者间的推导关系 aims at determining which are the correct coclusions of a gi
  • 关于软件形式化验证

    万次阅读 2018-05-29 09:37:01
    形式化验证是用逻辑来验证程序的可靠性,就是把一段程序用逻辑的方法证明一遍,证明它能得到预期的结果,没有bug。一般这类研究主要应用于昂贵的航天器材的操作系统、危险的医疗设备的程序之中。因为航天器材、医疗...
  • 随着平台级应用的普遍化,智能合约涉及的金额呈指数级别增长,如果其代码存在漏洞,则可能会遭到攻击,造成巨额损失,为防止类似事件发生,提出了运用形式化方法提高智能合约的安全系数的方法。 一、智能合约简介 ...
  • Javascript 模块化规范

    千次阅读 2018-08-06 19:48:49
    目前JavaScript领域广泛使用的模块化规范包括,commonJs规范、AMD规范,CMD规范。 今天简单介绍下这三种开发规范。 一、commonjs规范   commonjs出现的背景和JavaScript的函数式编程有关,没有标准化模块化系统...
  • 文章目录关系数据库关系数据库简介关系数据结构及形式化定义关系操作关系模型的完整性关系代数 关系数据库 关系数据库简介 美国????IBM公司的E.F.Codd 1970年提出关系数据模型E.F.Codd, “A Relational Model of ...
  • 关系模式的规范化理论

    千次阅读 2019-05-11 19:43:44
    关系模式规范化的定义 到目前为止,规范化理论已经提出了六类范式。范式级别可以逐级升高,而升高规范化的过程就是逐步消除关系模式中不合适的数据依赖的过程,使模型中的各个关系模式达到某种程度的分离。一个低一...
  • 形式化、半形式化和非形式化

    千次阅读 2008-07-25 12:38:00
    形式化规范就是用一套基于明确定义的数学概念的符号来书写,并且通常伴随着支持性的解释(非形式化)语句。这些数学概念被用来定义符号的句法和语义,以及支持逻辑推理的证明规则。支持形式化符号的句法和语义规则...
  • 通过对形式化方法特点分析,给出基于模型检验的设计规范提取步骤,以提高设计的正确性和完整性。以ARINC429总线传输模块设计为例,基于形式化方法完成正向设计过程。试验结果表明,基于形式化方法的设计流程能够有效...
  • 数据库关系的规范化

    千次阅读 2019-05-26 14:18:10
    在关系数据库中,所有的数据文件都以 二维表的形式...这种分解的过程就叫做规范化。 第一范式1NF 第一范式的目标是确保每列的原子性 如果每列都是不可再分的最小数据单元(也称为最小的原子单 元),则满足第一范...
  • 规范化Unicode字符串

    千次阅读 2020-07-05 11:07:13
    规范化Unicode字符串大小写折叠规范化文本匹配实用函数极端规范化:去掉变音符号 因为Unicode有组合字符(变音符号和附加到前一个字符上的记号,打印时作为一个整 体),所以字符串比较起来很复杂。 #café”这个词...
  • 数据规范化(归一)方法

    万次阅读 2017-06-22 09:03:38
    数据挖掘中,在训练模型之前,需要对特征进行一定的处理,最常见的处理方式之一就是数据的规范化。数据的规范化的作用主要有两个:去掉量纲,使得指标之间具有可比性;将数据限制到一定区间,使得运算更为便捷。
  • 本体(Ontology)概述

    万次阅读 多人点赞 2018-07-19 14:37:40
    认识本体  本体(Ontology)的概念源自于哲学领域,在哲学中的定义为“对世界上...德国学者Studer在1998年给出了本体的相关定义“本体是共享概念模型的形式化规范说明”。这个定义包含了四层含义:即共享(share)...
  • xml规范_XML规范形式介绍

    千次阅读 2020-06-22 17:46:25
    XML的传统在于文档领域,这在... W3C将此抽象模型形式化为XML Infoset(请参阅参考资料 ),但是许多XML处理必须着重于编码的源形式,这允许大量的词汇差异:属性可以以任何顺序出现; 空格规则在元素名称及其属性之...
  • C程序设计(第四版) 谭浩强 著 1:在该书P50浮点型数据中这样写道:在指数形式的多种表示方式中把小数部分中小数点前的数字为0、小数点后第1位数字不为0的表示形式称为规范化的指数形式,如0.314159*10^1就是3....
  • 本体研究综述(笔记版)

    万次阅读 2017-12-07 21:12:07
    张秀兰教授通过对国内外各领域本体定义的深入研究,总结出了本体定义:本体是通过描述、捕获领域知识,确定领域内共同认可的概念和概念间的关系,以用于领域内的不同主体之间交流与知识共享的形式化规范说明。...
  • 数据规范化的方法

    千次阅读 2019-04-22 18:56:38
    数据挖掘之数据规范化  数据规范化处理是数据挖掘的一项基本操作。现实中,数据中不同特征的量纲可能不一致,数值间的差别可能很大,不进行处理可能会影响到数据分析的结果,因此,需要对数据按照一定比例进行缩放...
  • 然后写加法运算的形式化规范,如下: {a:int8,b:int8} //   设置代码执行的前提条件,保证a和b的类型是8位有符号机器整数; {c = a + b;} //  加法运算的源码程序; {(int8.repr(a+b)) /\ ((Int8.repr (a+b)) = (a+...
  • 规范化、标准、归一、正则

    万次阅读 多人点赞 2018-07-18 21:52:39
    规范化: 针对数据库 规范化把关系满足的规范要求分为几级,满足要求最低的是第一范式...数据规范化是数据挖掘中的数据变换的一种方式,数据变换将数据变换或统一成适合于数据挖掘的形式,将被挖掘对象的属性数据按...
  • 什么是标准规范化,系统

    千次阅读 2014-10-08 11:36:31
    同时应包括对这种价值观的形式化描述集合,即原则。 原则用于指导形成方法论、判定行为或方法论是否符合价值。 4.如何实现这种思想体系的目的。即方法论。 方法论应符合价值观及其基础原则。方法...

空空如也

空空如也

1 2 3 4 5 ... 20
收藏数 377,632
精华内容 151,052
关键字:

形式化规范