形式验证

形式验证（通用4篇）

形式验证 篇1

如今超大规模集成电路 (IC) 的发展趋势加快了片上系统 (System-on-Chip, So C) 技术的开发, 而功耗管理与节能技术已经遍及片上系统设计的各个方面, 目的在于在电源占决定性作用的应用设备, 如有限电池寿命的移动通信终端以及大型消费电子类产品中得到有效的节能控制。降低功耗可以说贯穿了整个芯片的设计流程:从架构级设计, 寄存器传输级 (RTL) 实现到最终的物理设计。

然而, 随着硬件复杂度的增加, 其功能验证也面临越来越大的挑战, Jasper所推出的Jasper Gold低功耗验证产品主要解决节能芯片设计中的形式验证问题, 能有效地克服片上系统节能设计面临的验证挑战。

节能验证 (Power-Aware Verification) 面临的挑战

节能验证不仅要符合UPF (Unified Power Format) 或者CPF (Common Power Format) 规范, 全面地实施其规定的低功耗意图, 并且要保证在加入电源管理电路之后, 功能设计仍能正常进行。通常, 在设计流程的各个阶段都会实施功耗估算, 但精确的功耗估算只有在实体布局之后才能进行。因此, RTL和布局修改等会在设计流程中反复进行, 这种迭代功耗设计优化无疑增加了验证和调试的工作量、项目风险及成本。因此在限制成本的同时达到最优化功耗是我们设计的目标, 其面临以下技术挑战。

1.电源管理方案

首先要先设计一个独立实施的功能规范来满足产品需求, 然后根据软硬件进行功能划分。一个初级的电源管理方案可以设计在架构级层, 但是它仅定义对于给定的使用案例哪一种功能应该或者怎样被禁用。然后, 在RTL中实施功能设计, 其中需要广泛使用和多次利用已有的硅知识产权 (SIP) 模块或新的RTL块。一些模块的使用将会在软件栈的控制下进行。在这个阶段, 通过使用大量的降低功耗的方法如, 时钟门控技术 (Clock gating) , 动态压控变频 (Dynamic voltage-frequency scaling, DVFS) , 电源关断 (Power shut-off) , 内存访问优化 (Memory access optimizations) , 多供电电压 (Multiple supply voltages) , 片基电压偏置 (Substrate biasing) 等, 来得到必要的低功耗性能, 并决定应该释放哪些功能, 这些决定应在充分理解电路活动的基础上提出。但是这些早期的电源管理决定不能在布局布线 (P&R) 的时候决定最终的电路分区设计, 所以在P&R之后还要对其修改或者重新验证。很显然, 电源管理方案是一个动态的目标, 在设计流程的每一个阶段———架构级, RTL实施和物理实体设计都需要迭代设计优化、验证和重验证。

2.存在额外的复杂性

任何方案的实施都会明显受到一些额外复杂性的制约, 如 (a) IP的使用和重用的影响:通常, 给定的IP模块可以实施一些功能, 比如给电源控制寄存器或者信号增加接口等, 这些功能各自之间可以独立关闭。但对于第三方IP将会存在一个问题就是仅黑盒信息可用。因此, 任何情况下, 验证面临的挑战都包括重验证新制定的IP块以及电源管理电路两部分。 (b) 可测性设计 (Design-for-test, DFT) 电路的影响:为了最小化测试模式的计算以及测试时间, 常规的DFT假设整个芯片安装运行全部的功能, 即在运行的过程中, 测试和诊断也在同时进行。因此, 节能设计中DFT电路也必须符合设计的功耗管理策略, 避免过度的功耗和不必要的域丢失。

节能验证要求

功能分析、优化和验证贯穿了整个设计过程, 并由于第三方IP白盒功能可视化的不足而变得复杂, 因此一个低功耗方案必须包含以下五项主要要求:

(1) 在布线前后使用典型的波形进行有效精确的功耗估算;

(2) 在使用第三方IP之前对其白盒行为进行精确地可视化分析;

(3) 在集成前后进行合适的降低功耗技术的应用, 持续优化以及验证;

(4) 在功耗优化电路实施前后在架构级以及RT级进行彻底的功能验证;

(5) 进行与软件控制顺序一致的硬件功能性验证。

其中, 第一项要求可以用商用工具使用仿真和验证的方法处理。正如前面提到的, 电源管理方案是从架构级层开始的, 必须首先验证任何有用的架构特性如通信协议 (见图1) 。在随后的RTL流程, 根据有效的数据和优化需求, 低功耗管理设计被引入到So C开发的各个阶段。这里以电源域的配置举例, 优化必须保证正常的功能不受增加的电源域和电源控制逻辑所影响;电源域需在门控开关关闭之前保持正确的电源状态, 在输出或者给定激励时不产生额外的Xs (不确定态) ;对电源开关事件进行高层次的集中控制;关闭某个电源域不会破坏IP模块之间的连通性。因此, 把RTL模型看作是最重要的参考模型, 功耗验证需要将架构层验证、IP白盒功能可视化及分析、彻底的功能验证、控制和状态寄存器 (CSR) 验证、X-propagation分析、连通性检查等组合起来。

传统节能验证的局限性

在传统的电源节能验证过程中, 会存在一些局限性, 例如:经常会采用自动化结构分析、手工分析等手段来对电源管理电路进行分析, 这些分析手段可以确保RTL设计和UPF/CPF规范之间的一致性, 但不能验证设计的正确性;在架构级, 常采用人工电子表格的方式实施功耗分析, 效率低下;在RT级进行节能仿真, 速度很慢而且分析结果不详尽, 当加入复杂的电源管理方案后导致的状态空间扩张还会更进一步降低仿真性能;和电源相关的设计性规则检查 (DRC) 只能在门级提供有限的电源完整性分析等。

因此, 传统的节能验证方法只能提供有限的分析和验证可靠性, 达不到良好的结果品质 (Qo R) 。

Jasper Gold应用满足节能验证需求

Jasper Gold节能验证流程能全面地满足功耗验证需求并达到较佳的Qo R, 如图2所示。在流程的前端是Jasper Gold的低功耗验证, 它能自动进行节能转换, 同时产生一个节能模型并对电源域、供电网 (Power Supply Net) 、隔离规则和数据保持规则进行标识。通过从UPF/CPF规范, RTL代码, 以及任何用户定义的断言中解析提取相关数据, 然后自动产生可以被其它Jasper Gold应用所使用的断言, 这些应用一般用来验证功耗降低和电源管理电路是否符合UPF/CPF规范以及是否会对最初的RTL功能产生负面影响等。

a.电源节能模型

Jasper Gold电源节能模型能保证对一系列广泛的电源管理特性的分析验证。如:1) 电源域的正确性;2) 电源状态表的稳定性, 分析各种电源状态转换并检查不合法的状态;3) 状态保持单元验证, 验证所有电源状态的完整性;4) 供电网间的连通性, 检查在定义供电网的时候是否产生功耗意图错误;5) 节能设计的正确性, 当所有的电源域连续起作用时, 保证电源节能设计和最初的RTL之间的等价性。

b.低功耗验证产生的断言

Jasper Gold低功耗验证程序产生的断言包括:在域的电源打开或者关闭的过程中保证此电源域无效;当存储某一个元素的值时, 相应的状态存储逻辑电源应该打开;无论何时电源域关闭, 所有和电源域相关的隔离条件在电源关闭之前、关闭过程中以及关闭之后都视为真;在相反的钳位值下信号不能被隔离两次等。

c.Jasper Gold应用套件

与一般的一体化的形式验证方法相比, Jasper Gold方案支持步进的形式验证。Jasper Gold应用能提供执行某种特定任务所需的全部功能工具和形式化方法。这种应用方案要求设计团队仅具备其当前进行的任务所必需的专业知识即可。Jasper Gold应用套件主要包含:

(1) 架构验证:用于分析验证对节能设计的实施产生影响的架构特性, 如通信协议等。

(2) RTL开发:运用行为索引技术分析不熟悉的RTL模块, 比如分析第三方IP模块得到其有效的白盒行为, 然后对之修改加以使用。该应用支持用户在整个流程中设计、修改、验证RTL代码并将其中的改变可视化。

(3) 形式属性验证 (FPV) :对电源管理电路以及在添加电源管理电路之前对某个或者所有的RTL功能执行详尽的验证。比如在时钟设计和集成之后分析通电次序、状态正确性和安全性, 如时钟失灵, 模块隔离和电源关闭等。

(4) 控制和状态验证:验证设计是否遵守控制和状态寄存器 (CSR) 规范, 在电源管理插入前后从寄存器读的值是否总是正确等。

(5) 时序等价验证:验证电源管理电路插入前后, 以及经后期修改的模块的等价性, 并且它可以验证内存优化不与性能相冲突, 比如, 当两个低功耗的存储器代替一个普通存储器时, 它可以证实前后存储模型在性能上是等价的。

(6) X-Propagation应用:分析验证由关电引起的Xs输出, 并且比较在实施UPF/CPF规范前后Xs的不同。

(7) 连通性验证:彻底地验证模块和单元级以及集成之后的RTL连通性。

总结

Jasper Gold节能验证流程可以对集成电路节能设计进行详尽的分析验证, 相比于传统的自动化结构分析和手工分析验证方法可以得到更佳的结果品质 (Qo R) ;并且, 利用Jasper Gold低功耗设计验证程序可以自动生成节能模型和合适的断言;同时, 设计流程运用一系列具有特定功能的应用组件, 使得设计团队可以根据需求选择合适的应用工具。

形式验证 篇2

公司介绍

Jasper是一家私营的自动化电子设计 (EDA) 公司, 它运用独有的形式技术, 为电子系统和半导体的设计与验证提供高价值、高投资回报率的解决方案。该公司于2005年1月收购了瑞典Safelogic公司, 从而实现对设计意图和执行的双验证。

近日, Jasper被美国著名科技企业杂志《Red Herring》誉为北美百强企业之一, 其“边设计边验证”的形式验证解决方案已经成功地应用于150多个芯片项目。Jasper公司的系统架构师、逻辑设计师、验证工程师和芯片设计团队在这一技术的帮助下, 可以顺利地调试架构规范, 设计并探索RTL (寄存器传输级) 工程, 验证SOC片上协议和级块功能的正确性。此外, Jasper技术还可以帮助逻辑设计师对基于行为的RTL进行分析和验证, 加快知识传播的速度, 改善维修流程, 实现高效的重复使用。无论是对新手还是对高级用户, Jasper解决方案都具有极高的应用价值。

Jasper以逻辑设计师为目标客户, 开发了可用于确认和检索预期功能行为的新技术, 旨在帮助逻辑设计师轻松地验证复杂的设计和行为间的相互作用。这一应用模式有时也被称为“设计师自主检验”, 其强大的智能分析功能可以帮助设计师和验证工程师, 在不向原设计者进行咨询的情况下, 将升级后的设计与相关功能无缝整合在一起。Jasper技术的这一能力使得整个生命周期中的任何用户都可以理解、修复并重新定位RTL设计。

不依赖仿真的“纯”形式验证

1. Jasper Gold形式技术

(1) 什么是形式验证

在介绍Jasper Gold形式技术之前。我们先来了解一下什么是形式验证。

在当前复杂的数字设计开发过程中, 功能验证十分重要。根据Collett International Research作的一项调查表明, 只有39%的设计在第一次验证时没有缺陷, 60%包含逻辑或功能缺陷, 20%以上需要三次或者多次验证。若在设计过程后期才发现前期的设计错误, 更正的代价非常高, 除了费用增加、丧失市场机会外, 有时甚至会导致项目被迫中断。若在软件发布后才发现设计的不合理, 则更新和维护的成本更是让企业难以承受。由于设计的整体复杂性不断增加, 设计验证任务也随之变得复杂, 硬件验证本身越来越具有挑战性, 而且验证时间正在变得越来越长。根据另外一项Collett调查显示, 高达50%的设计开发时间和资源花在功能验证上, 验证已被公认为是设计过程中的主要瓶颈。尽管如此, 花费诸多时间和资源进行功能验证和改进设计仍然是必要的, 它能帮助企业减少错误、缩短软件推向市场的时间、降低整体成本。

形式验证的主要思想是通过形式化方法来验证一个设计的功能是否正确。所谓形式化方法是指基于严格定义的数学概念和语言进行设计, 语义清晰, 无歧义, 可以用自动化或半自动化的工具进行检查和分析, 而传统的方法则基于自然语言, 语义含糊, 无法进行检查。因此, 形式验证以清晰的数学定义为基础, 大大提高了验证的准确性, 有效降低了设计的风险。

(2) Jasper Gold形式验证技术

Jasper Gold是Jasper公司最重要的专利之一, 其借助形式化技术平台, 创建了业内最顶尖的验证解决方案。这一方案具有无缝可扩展性, 既适用于基于断言的验证方法 (ABV) , 也可以用于针对微架构性能的端到端详尽验证。Jasper Gold技术整合了自动形式记分牌技术 (automated Formal ScoreboardTM) 、验证加速技术 (Proof AcceleratorsTM) 和Proof Grid技术, 可以对各种复杂的设计 (包括基于分组的数据传输、先入先出的执行操作 (FIFO) 、存储、高速缓存和多时钟域) 进行准确的验证。借助于强大先进的形式化专利技术和业内最高级的核心处理引擎, Jasper Gold技术提供了卓越的形式验证功能。Jasper的技术是基于一种据称可突破容量限制的“预识别引擎”。它之所以能实现这一点, 是借助了“状态-空间隧道”技术, 该技术引导形式验证引擎只分析与验证与每项需求有关的那部分设计。因此, Jasper Gold不像其它形式工具那样被限制在一个小的验证半径范围内。此外, 利用JasperGold上下文相关的可视性验证功能和互动技术, 用户能够对关键的设计功能的正确性进行验证。这种互动技术是采用“关联指示” (relevance directive) , 以允许用户指导预识别引擎的工作, 类似于底层规划工具对布局和布线的指导。“用户就像在与工具玩游戏”Tempus Fugit的创始人、现任Jasper公司工程副总裁的Vigyan Singhal形容道, “通过用户与工具之间的互动, 工具能更准确地判断从哪里切入设计。”

Jasper最新的行为索引技术在设计理念上实现了重大突破, 能促进RTL设计质量的提高和设计师生产能力的提升。用户在行为索引技术的帮助下, 可以在一个动态的、可执行的数据库里, 反复提取、检索和存储相关的设计行为。针对复杂而灵活的基于行为的分析和动态回归, Jasper对这一行为索引技术进行了优化, 使其可以与形式化技术平台 (Jasper Gold) 无缝拼接, 共同发挥作用。

(3) Jasper Gold应用

Jasper公司基于Jasper Gold形式验证技术, 开发了专门针对解决具体设计问题和验证难题的解决方案———Jasper Gold应用。Jasper Gold是一款突破现有容量限制的“纯”工具, 而且该工具非常易于使用。它超越了接口的范畴, 承诺能根据高层次的规范级需求以及低层次的声明进行详尽的模块级验证。虽然许多供应商已经采用需要使用仿真的“半形式”验证方法, 但Jasper公司认为不依赖仿真的“纯”形式验证才是有前途的方法。

通过一个共享的数据库, JasperGold应用能与其它多种应用一起无缝工作, 从而做到:

●设计团队可以通过一个普通的数据库, 在各个应用程序中共享设计作业;

●可以通过一个公共接口, 启动并行的应用程序;

●简化各个应用程序之间的接口。

此外, 通过与Jasper Gold应用程序的无缝合作, 其它应用程序的效率得到了提高, 具体表现在以下几个方面:

●程序的配置变得更加灵活;

●用户可以充分发挥整个服务器机群的作用;

●在同一个级块中运行多个应用程序。

2. 产品———智能验证工具包

在当今So C设计日趋复杂的背景下, 为确保协议规范的一致性, 对诸如AMBA, AXI, PCI-Express等标准协议的验证变得更加地困难和费时。此外, 这也增加了验证工程师对设计团队的依赖性。

虽然So C的设计团队经常会花费数周的时间, 对标准接口协议 (如AM-BA和PCI-Express) 进行验证, 但是由于协议规范文件描述上的模糊性和非穷尽的仿真方法, 还是会出现错误和缺陷。为尽可能避免设计错误, 需要工作人员能掌握相关专业知识, 并正确地理解协议规范。然而, 在实践中, 我们往往很难在设计周期的早期就模拟设计行为。

Jasper智能验证工具包 (简称为IPKs) 和智能验证解决方案可以对标准协议进行快速和穷尽的验证, 从而帮助So C设计团队加快验证进程。Jasper创建的协议规范内置了具体的属性定义, 因而在早期就可以对设计进行验证。

此外, Jasper智能工具包还可以无缝地应用到模拟环境中, 并与JasperGold属性形式验证程序无缝拼接 (如图2所示) , 共同发挥作用, 对嵌入式协议属性进行形式化验证, 从而能对设计进行穷尽验证, 确保其符合设计规范。借助智能工具包, 设计人员无需再手动输入协议属性。

正如图3的流程图所示, 智能工具包作为Jasper Gold技术平台的一部分, 也可以在该平台上使用。在Jasper Gold RTL开发App以及JasperGold形式属性验证App的共同作用下, 用户可以将时序图和协议交易的过程可视化, 从而能更直观地理解属性行为和设计规范。智能验证工具包可以自动生成Tcl (工具命令语言, 经常被用于快速原型开发、脚本编程、GUI和测试等方面) 文件和封装器, 其中包含了自定义验证工具包的源代码, 以及为形式化属性验证所配置的各种指令。

3. 服务

Jasper清楚地了解, 一家成功的EDA公司不仅仅是产品的提供者, 同时也应成为其客户的合作伙伴。长期以来, Jasper已经建立了一套成熟完善的客户服务体系, 为客户提供卓越的技术支持, 包括方法咨询和专业培训。此外, Jasper还开发了一整套的证明工具包, 以及一系列的配套服务, 以确保客户能成功地进行项目验证, 达到预定的目标投资回报率 (ROI) 。

(1) 培训

Jasper提供的培训课程覆盖了客户应用Jasper解决方案的整个周期, 培训内容包括软件语言的属性讲解以及验证方法的阐述。Jasper的培训课程非常丰富, 包括asper Gold标准培训、Jasper Gold高级培训、使用Jasper Gold验证系统对高层次需求进行完整证明的入门介绍, 使用属性描述语言 (PSL) 进行基于断言验证 (ABV) 的入门介绍等。

(2) 咨询

Jasper为满足客户的定制性需求, 提供了灵活的现场咨询服务。Jasper致力于帮助客户结合形式验证和传统仿真法, 将合适的解决方案成功地应用于设计过程里的每一个问题中。

小结

Jasper公司通过为客户提供的形式验证技术, 极大地加强了客户在整个片上系统 (So C) 的设计周期中的竞争优势, 降低了设计成本, 缩短了设计周期, 减少了设计风险。

“现在, 我们才真正起步。”Jasper总裁兼首席执行官Kathryn Kranen表示, “我们正在利用所掌握的标准接口知识, 并为工具内建以往具有博士学位的用户才能达到的智能。”她宣称, Jasper的技术是第一次真正的突破, 它同时解决了容量和易用性问题。“我们正在捍卫形式验证的荣誉, ”她说, “大多数公司不能达到100%彻底验证的目标。”

形式验证 篇3

随着数字化变电站的发展,基于IEC 61850的变电站自动化是一种必然趋势[1]。电网结构日趋复杂、容量不断扩大、实时信息传送量成倍增多,对变电站智能电子设备(IED)提出了更高的要求。新开发的IED必须具备高效快速的处理能力,以满足大量信息传输的实时性、可靠性和多任务性。目前,新型的IED多采用数字信号处理器(DSP)+ARM(advanced RISC machines)双中央处理器(CPU)结构[2],甚至出现了集成多功能的集中式IED[3]。随着硬件可靠性的提高,IED的可靠性越来越依赖嵌入式软件的质量。IEC 61850为变电站内IED之间的互操作提供途径,其应用的关键在于利用标准的模型对实际的IED进行建模,将其功能抽象成若干逻辑节点(LN),以达到信息交换的目的[4]。为了更好地实现分布式功能在IED上的标准化设计,需要事先对各种功能在IED之间和IED内部LN之间的交互关系、系统行为进行严谨描述与验证,以保证分布式功能的正确性[5]。

已有相关文献研究了基于IEC 61850的各种IED的设计开发方法。文献[1]研究了IEC 61850下间隔层IED软件设计方案,分析了IED的功能模型。文献[6]给出了保护功能一般性建模方法,但仍很抽象。文献[7]研究了基于IEC 61850的变压器IED的设计,以模块化的方法设计了IED嵌入式软件。文献[8]基于面向对象的方法对线路电流差动保护IED进行设计。文献[9]依据IEC 61850,建立了牵引变电站线路保护IED的对象模型。文献[10]利用配置文档动态地生成IED的模型。文献[11]研究利用可编程逻辑语言的与门、或门对IED内部的 LN之间关系进行可视化设计,但未能完整地描述和严谨地设计IED之间和IED内部各LN 之间的逻辑关系。电力系统IED是一种系统行为与时间紧密相关的嵌入式系统,其设计、实现与验证比较复杂。已有文献中,IED的开发过程缺乏对系统行为的有效建模,以及在设计阶段对系统关键行为进行分析与检验等方面的研究工作。

通信顺序进程(CSP)[12]是Hoare于1978年建立的一种适合于分布式并发软件规格和设计的形式化方法,已经广泛地应用于软件的行为建模。它以进程的方式刻画系统的动态行为,具有强大的描述能力。已有基于CSP的验证工具——进程分析工具包(PAT)[13]可以对系统中的死锁、活锁、可达性等安全问题进行自动化验证。在CSP基础上加入时间相关操作而形成的一种形式化语言Timed CSP[14],能够对实时的并发系统进行良好的描述。本文采用Timed CSP对IED内各LN的交互关系、系统行为进行描述并验证,进而指导IED的软件设计和互操作测试实验。

1Timed CSP简介

Timed CSP中最基本的概念是事件和时间。通常用小写字母a,b,c或自定义字符串表示事件。事件的序列形成进程,通常用大写字母P,Q或自定义字符串表示。√是一种特殊的事件,表示进程正常终止。时间用字符t或数字表示。

Timed CSP定义的巴克斯范式如下:

P::=stop|skip|wait$t|\text{a}\to \text{Ρ}|\text{a}\stackrel{t}{{\displaystyle \to }}\text{Ρ}|\text{Ρ}$;Q|P□Q|P∏Q|a:$A\stackrel{t}{{\displaystyle \to }}\text{Ρ}{}_{\text{a}}|\text{Ρ}\stackrel{t}{{\displaystyle ⊳}}\text{Q}|\text{Ρ}\text{Δ}\text{Q}|f(\text{Ρ})|\Vert {}_{A{}_{\text{Ρ}}}\text{Ρ}|\text{Ρ}{}_A\Vert {}_B\text{Q}|\text{Ρ}\underset{C}{{\displaystyle \parallel }}\text{Q}|\text{Ρ}|||\text{Q}|\text{Ρ}A|\mu X\cdot F(X)$

上述定义解释如下。

stop:停止,表示一个进程的中断,该进程不与外部发生通信,可表示死锁或进程不收敛。

skip:跳过,表示一个进程除终止外不做任何事情。

wait t:等待,表示进程在时间t后终止,其间不做任何事情。

$\text{a}\stackrel{t}{{\displaystyle \to }}\text{Ρ}$:前缀操作,表示事件a经过时间t执行完后执行进程P。

P;Q:顺序复合,表示进程P执行完后执行进程Q。

P□Q:外部选择,表示执行进程P或Q依赖于进程执行的第1个事件。

P∏Q:内部选择,表示执行进程P或Q由进程内部决定。

a:$A\stackrel{t}{{\displaystyle \to }}\text{Ρ}{}_{\text{a}}$:通道选择输入,a为A中的任一事件,a的类型由通道输入的数据类型决定。

$\text{Ρ}\stackrel{t}{{\displaystyle ⊳}}\text{Q}$:超时,如果时间t内2个进程未发生通信则认为超时,控制权由P交给Q。

PΔQ:中断,Q的任何事件执行都能导致P 的中断。

f(P):换标,f(P)和进程P有着同样的结构,只是P中的事件经过函数f映射为另一个名字。

‖APP:同步并发,P的所有子进程必须执行AP中的所有事件且每一对子进程同步执行它们的事件集合交集上的事件。

PA:集合隐藏,表示不显示进程P中任何属于A的事件。

$\text{Ρ}{}_A\Vert {}_B\text{Q}$:同步并发,P仅能执行A中的事件,Q仅能执行B中的事件,A∩B的事件P与Q同步执行。

$\text{Ρ}\underset{C}{{\displaystyle \parallel }}\text{Q}$:同步并发,P和Q在集合C的事件并发,在其他集合的事件交叉进行。

P|||Q:异步并发,进程所执行的每个事件为进程P或Q中的一个事件。

μX·F(X):X是一个进程变量,A=αX,F(X)称为包含进程变量X的一个前缀表达式,且该递归方程具有事件符号集A上的唯一解。

例如:下文中PTOC:=strop$1\stackrel{t{}_1}{{\displaystyle \to }}\text{s}\text{t}\text{r}\text{o}\text{p}2\stackrel{t{}_2}{{\displaystyle \to }}\text{s}\text{t}\text{r}\stackrel{t{}_3}{{\displaystyle \to }}\text{Ρ}\text{Τ}\text{Ο}\text{C}$就是这种表示法。其中,A={strop1,strop2,str};X为进程变量PTOC;F(X)为前缀表达式strop$1\stackrel{t{}_1}{{\displaystyle \to }}\text{s}\text{t}\text{r}\text{o}\text{p}2\stackrel{t{}_2}{{\displaystyle \to }}\text{s}\text{t}\text{r}\stackrel{t{}_3}{{\displaystyle \to }}\text{Ρ}\text{Τ}\text{Ο}\text{C}$。Timed CSP更详细的操作语义可参见文献[12]。

2 IED逻辑模型与Timed CSP的转换关系

IED是IEC 61850中保护功能的设备载体,LN是最基本的功能单位。对于IED的设计,必须关注它所包含的LN如何正常工作并完成所分配的分布式功能,进一步从全貌和细节角度对分布式功能下各IED之间、IED内部相关LN之间的交互关系进行严谨刻画,从而实现IED程序的标准化设计。

根据IEC 61850,LN间通过逻辑连接(LC)相连,专用于LN间的数据交换。因此,LN之间的交互表现为它们之间的数据交换,即消息传递。将LN定义为进程,与LN有关的消息定义为进程的事件集。IED之间、IED内部相关LN之间的交互关系就是进程之间的交互关系,这种关系即是进程之间消息的传递。LN的输入可表示为从其他LN接收到的消息。每个进程按照自己的行为发送和接收消息,进程之间独立并行地运行。为了利用Timed CSP描述IED逻辑交互模型,需要将IED逻辑模型转换为Timed CSP描述的规格。

根据Timed CSP操作语义及IEC 61850中IED的逻辑节点模型,与本文描述有关的映射关系描述如表1所示。

3 实例分析

3.1 IED交互模型

为了能够清晰地表达出一个分布式功能下各IED之间的关联关系(如信息传递、函数调用、事件触发等)、交互信息(包括调用消息、变化量、事件等信息的内容及其通信要求)、交互发生的先后次序,在IEC 61850-5[15]的基础上,建立定时过电流保护的交互模型如图1所示。

该模型包含的LN有定时过电流保护PTOC、跳闸条件PTRC、断路器XCBR、自动重合闸RREC、扰动记录RDRE、故障记录RFLO、开关控制器CSWI、人机接口IHMI、告警处理CALH等。其中,PTRC用于组合各种跳闸信号,构成一个跳闸信号条件,这里只考虑PTOC这一个跳闸信号。图1中标出的各逻辑节点之间传输信号的时限参考文献[15]。各IED的LN交互过程如下。

1)PTOC检出故障后,使其启动状态Str=1、跳闸状态Op=1,传给PTRC(消息流①),PTRC接收处理后,发出跳闸通用面向对象的变电站事件(GOOSE)报文XCBR.Pos.ctlVal=off 给XCBR和RREC(消息流②),以跳闸和启动重合闸。

2)PTOC将其保护启动信息Str=1,PTRC将其跳闸信息Tr=1分别以报告形式发送给站级的CALH(消息流③和④),同时将其保护启动信息Str=1发送给录波IED中的RDRE和RFLO(消息流⑤),以启动扰动记录。

3)XCBR接收跳闸报文,经附加处理后跳开断路器。当断路器的状态XCBR.Pos.stVal由合变成开时,用GOOSE报文立即发送新状态XCBR.Pos.stVal=off给PTRC和 RREC(消息流⑥)。断路器的变位信息以报告模型报告给测控IED中的CSWI(消息流⑦),CSWI再将此报告传给站级主机的IHMI(消息流⑨)。

4)RREC尝试以不同延时重合已跳开的断路器,发出带值重合闸的GOOSE报文XCBR.Pos.ctlVal=on给XCBR(消息流⑧),发送报告RREC.Op=1给IHMI (消息流⑩)。

5)XCBR接收带值重合闸报文,经处理合上断路器,如果是临时性故障,则断路器合上,送出断路器新状态的GOOSE报文XCBR.Pos.stVal=on给PTRC和RREC(消息流(11))。类似地,产生断路器合上的XCBR到CSWI和CSWI到IHMI的报告(消息流(12)和(13))。

3.2 IED交互模型的形式化描述

根据IED逻辑模型与Timed CSP的转换关系,图1中有9个LN进程,进程名即为LN的名称。LN上的动作(包括发出消息和接收消息)为LN进程的事件集,每个动作的时限即为相应事件规定的完成时间。

事件即为消息名,发送消息与接收消息相同时,用一个事件来表示。2个进程的事件集中有相同的事件,即表明进程存在交互行为。按照Timed CSP中的表示法,图1中相关进程的事件集如表2所示。

各进程的交互行为描述如下。

PTOC::=strop$1\stackrel{t{}_1}{{\displaystyle \to }}\text{s}\text{t}\text{r}\text{o}\text{p}2\stackrel{t{}_2}{{\displaystyle \to }}\text{s}\text{t}\text{r}\stackrel{t{}_3}{{\displaystyle \to }}\text{Ρ}\text{Τ}\text{Ο}\text{C}$

RDRE::=str$\stackrel{t{}_3}{{\displaystyle \to }}\text{R}\text{D}\text{R}\text{E}$

PTRC::=strop$1\stackrel{t{}_1}{{\displaystyle \to }}\text{g}\text{o}\text{o}\text{s}\text{e}\_\text{o}\text{f}\text{f}\stackrel{t{}_4}{{\displaystyle \to }}\text{t}\text{r}\stackrel{t{}_2}{{\displaystyle \to }}\text{Ρ}\text{Τ}\text{R}\text{C}\square$

goose_on_off$\stackrel{t{}_4}{{\displaystyle \to }}\text{Ρ}\text{Τ}\text{R}\text{C}$

XCBR::=goose_off$\stackrel{t{}_4}{{\displaystyle \to }}\text{g}\text{o}\text{o}\text{s}\text{e}\_$off_on$\stackrel{t{}_4}{{\displaystyle \to }}\text{x}\text{c}\text{b}\text{r}\_\text{s}\text{t}\text{v}\text{a}\text{l}\stackrel{t{}_2}{{\displaystyle \to }}\text{X}\text{C}\text{B}\text{R}\square$goose_on$\stackrel{t{}_4}{{\displaystyle \to }}\text{g}\text{o}\text{o}\text{s}\text{e}\_$off_on$\stackrel{t{}_4}{{\displaystyle \to }}$

xcbr_stval$\stackrel{t{}_2}{{\displaystyle \to }}\text{X}\text{C}\text{B}\text{R}$

RREC::=goose_off$\stackrel{t{}_4}{{\displaystyle \to }}\text{g}\text{o}\text{o}\text{s}\text{e}\_\text{o}\text{n}\stackrel{t{}_4}{{\displaystyle \to }}\text{g}\text{o}\text{o}\text{s}\text{e}\_$off_on$\stackrel{t{}_4}{{\displaystyle \to }}\text{o}\text{p}\stackrel{t{}_2}{{\displaystyle \to }}\text{R}\text{R}\text{E}\text{C}$

CSWI::=xcbr_stval$\stackrel{t{}_2}{{\displaystyle \to }}\text{i}\text{h}\text{m}\text{i}\_\text{s}\text{t}\text{v}\text{a}\text{l}\stackrel{t{}_2}{{\displaystyle \to }}\text{C}\text{S}\text{W}\text{Ι}$

CALH::=strop$2\stackrel{t{}_2}{{\displaystyle \to }}\text{t}\text{r}\stackrel{t{}_2}{{\displaystyle \to }}\text{C}\text{A}\text{L}\text{Η}$

IHMI::=op$\stackrel{t{}_2}{{\displaystyle \to }}\text{Ι}\text{Η}\text{Μ}\text{Ι}\square$ihmi_stval$\stackrel{t{}_2}{{\displaystyle \to }}\text{Ι}\text{Η}\text{Μ}\text{Ι}$

其中,t1<0.1 ms,t2<100 ms,t3<1 000 ms,t4<3 ms。

对各LN进程进行同步并行组装,即可完成系统的行为描述。

SYSTEM::=PTOC‖PTRC‖RDRE|XCBR‖CSWI‖RREC‖CALH‖IHMI

3.3 IED交互模型的形式化验证

PAT[13]是由新加坡国立大学开发的基于CSP的模型检测工具,包含CSP模型、实时系统模型、Web服务模型、概率模型等多种模型检测。PAT已被认为是良好的进程代数检测工具,支持可视化模拟、可达性分析、死锁检测等,且仍在不断发展完善。

将3.2节IED交互模型的形式化描述在PAT中进行验证,以0.1 ms为一个计时单元。首先将IED交互模型的形式化描述编辑在PAT主窗口中。编辑窗口中除了模型的描述外,还包括进行验证的断言,如附录A图A1中以#assert开头的语句。然后进行语法检测,以检测描述文本中的语法错误,最后点击“验证”,弹出的验证窗口见附录A图A1。

在附录A图A2的验证窗口中,可以对每一个断言进行验证,验证结果在输出窗口显示,显示的死锁验证结果为“The Assertion (System() deadlockfree) is NOT valid”,可见系统存在死锁。

经检查,RREC进程的描述存在不符合逻辑的情况。RREC接收任何一个消息,都会将其状态以op消息报告给IHMI,这些消息之间的关系是根据接收的不同消息来决定op消息的内容。所以,RREC接收的消息之间的关系应该为外部选择。将RREC的行为描述修正如下:

RREC=goose_off$\stackrel{t{}_4}{{\displaystyle \to }}\text{o}\text{p}\stackrel{t{}_2}{{\displaystyle \to }}\text{R}\text{R}\text{E}\text{C}\square$goose_on$\stackrel{t{}_4}{{\displaystyle \to }}$

$\text{o}\text{p}\stackrel{t{}_2}{{\displaystyle \to }}\text{R}\text{R}\text{E}\text{C}\square$goose_off_on$\stackrel{t{}_4}{{\displaystyle \to }}\text{o}\text{p}\stackrel{t{}_2}{{\displaystyle \to }}\text{R}\text{R}\text{E}\text{C}$

将修正后的描述再进行死锁验证,结果正确。

进行死锁验证的同时,可验证可达性。例如:当PTOC检测到故障时,发出strop1消息,验证XCBR能否在限定的时间内执行goose_off事件。当PTOC检测出故障,在0.1 ms内将故障信息发给PTRC,PTRC接收处理后,发出跳闸GOOSE报文XCBR.Pos.ctlVal=off给XCBR,XCBR跳开断路器。根据文献[15]中关于报文类型和性能的描述,这个过程的时间限为3.1 ms。在PAT中设定一个计数变量x,以0.1 ms为一个计时单元,上述过程的时间限为31个时间单元。时限目标:#define goal x≤31。可达性目标:strop1→<>goose_off。限时可达性目标:strop1→<>goose_off&&goal。验证结果见附录A图A3,输出窗口显示的验证结果为“The Assertion (System()=[]strop1→<>goose_off&&goal) is VALID”,表明断言是合法的,即验证了可达性。如果设置时限目标为#define goal x<40,输出同上面。如果将时限目标设置为:#define goal x<20,则验证结果为“The Assertion (System()=[]strop1→<>goose_off&&goal) is NOT valid”。也可以用同样的方法验证其他消息流的可达性,例如strop1→<>ihmi_stval。这个过程表示PTOC发出strop1给PTRC,PTRC接收后发出goose_off给XCBR,然后XCBR向CSWI报告goose_off_on,CSWI最后向IHMI报告ihmi_stval。以此来说明形式化描述是否真实地反映模型的交互过程。

从上述对IED交互模型的形式化描述及验证可以看出,将IED中LN的交互行为进行形式化描述并进行自动验证,可以在IED软件设计早期及时发现描述中的缺陷,有效地指导IED软件系统的设计并节约开发成本。

4 结语

IEC 61850产品设计仅靠常规的手工建模和编程,会使复杂的IED交互系统中存在隐含的缺陷,并制约系统的工程实施。本文从分布式功能建模和 IED 设计的角度出发,采用进程代数形式化方法描述保护功能下各IED之间和IED内各LN之间的交互模型,并进行自动验证,为基于IEC 61850的IED系统标准化设计提供良好的模型基础和方法,为工程应用提供一定的参考和借鉴,在一定程度上促进设计的规范化并及时发现系统中存在的缺陷,节约开发成本。

附录见本刊网络版(http://aeps.sgepri.sgcc.com.cn/aeps/ch/index.aspx)。

摘要：IEC 61850将变电站智能电子设备(IED)的功能抽象成若干逻辑节点,以达到信息交换的目的。IED及其逻辑节点之间的交互关系复杂,如何正确地设计并实现这种复杂的行为是IEC 61850实施的关键。形式化方法为此提供了良好的途径。提出采用进程代数方法对各种功能在IED之间、IED内部逻辑节点之间的交互关系、系统行为进行严谨地描述并进行自动验证,以保证分布式功能的正确性。以定时过电流保护功能为例,建立了基于IEC 61850的IED交互模型,采用在通信顺序进程(CSP)上加入时间相关操作形成的形式化语言Timed CSP描述其交互功能及系统行为,在验证工具——进程分析工具包(PAT)环境中进行了验证。结果表明,所提出的方法能有效地检测出描述中潜在的缺陷,有利于指导IED交互系统的设计并节约开发成本。

形式验证 篇4

节点自身定位是整个无线传感器网络(WSN文献[1][2][3])应用的一个支撑技术之一,由于节点自身定位过程容易遭受到来自内部和外部的攻击,又由于WSN节点自身资源的限制,所以在受限的WSN中,如何进行安全的定位和获取正确的位置信息,是一个非常具有挑战性的安全问题。

2 多点验证协议

可验证测距协议是一种采用基于测距的距离界定协议,不只可以用于抵抗各种距离攻击,还可以对节点进行安全定位。

2.1 距离界定协议

距离界定最早由Brands和Chaum提出(文献[4]),其基本思想是通过测量和计算验证者(verifier)与被验证者(claimant)之间距离的上界,防止以缩小测量/估算距离为目的的测距欺骗攻击,如虫洞攻击等。

2.2 距离界定协议

多点验证协议是一种改进型的距离边界协议,采用记录收发时间的策略来降低对被验证者实时处理能力的要求。其伪代码(如图1)所示,其中u是待验证节点(普通节点),v为验证者(信标节点),tus/tur和tvs/tvr分别是u和v发射和接收信号的时刻。

3 可验证测距协议的形式化研究

多点验证协议是一个基于距离界限协议的VM机制。VM利用可验证测距协议和三角形校验技术来提高测距安全,前者将基于RF的TOA技术[文献6]和距离界限协议[文献4]结合起来,能有效抵抗各种缩短测距的攻击,而后者在前者的基础上利用3个校验点的共同约束可以防止增大测距的攻击。下面我们将用形式化语言object-z(文献[5])对其展开建模研究分析。

3.1 可验证测距协议的模型组件

3.1.1 定义数据类型

我们假定给定的ITEM为会话层构造的比特流或字节流。所有信息的MSG的集合是所有可能的消息队列的集合,有MSG:seq ITEM。据此,我们定义几个在协议中使用的不同数据项类型ITEM的子集,代理标识符AID,密钥KEY,随机数NON:,加密数据ENC,如下图所示,P ITEM表示ITEM的子集。

3.1.2 定义函数模型

函数enc表示信息MSG经过密钥KEY加密成ENC类型数据项。函数mac表示信息MSG经过密钥KEY通过消息认证生成MAC类型数据项。函数commit表示随机数NON使用信息MSG单向抗碰撞哈

3.2 多点验证协议的角色模型

多点验证协议的角色模型正如前文表示可抽象成两种类型:Claimant待验证节点和Verifier验证者,使用object-z对两个角色进行建模,每个角色是类对象,包含状态变量和操作模式。

3.2.1 待验证节点的模型

待验证角色由状态模式、初始状态、操作模式GenerateC和操作模式ReceiveMsg组成的。状态模式定义该角色用到的变量,其中u、v为设备标识(u表示待验证节点,v表示验证者),Nu、Nv分别表示u、v产生的随机数,以及u和v共享的密钥Kuv,以及消息msg、c和d,时间t。初始状态msg=<>表示没有任何消息在发送。

操作模式GenerateC对应图1的1、2、3,表示验证者对确认者发起距离界定请求。其中,符号“!”表示请求的信息,符号“?”表示要求得到的信息。操作模式ReceiveMsg对应图1的6、7,表示对信息进行加密,对应于图1的5的接收。其中,变量t和t`表示前状态变量和后状态变量,表示时间变化。

3.2.2 验证者模型

验证角色由状态模式、初始状态、操作模式GenerateNv和操作模式Compute组成的。

操作模式GenerateNv对应图1中的4、5,表示对验证者对验证者的请求进行响应。操作模式Compute对于图1中的8、9,表示根据结果,验证本次通信是否被篡改,如果没有就进行距离计算。

3.3 多点验证协议模型

对角色建完模之后首先建立距离界定协议,由状态模式、初始模式和操作Protocol组成。表示通过待验证对验证者发起请求得到与其中一个验证者的距离信息。

在状态模式中,待验证者N ode A,验证者N ode B,N ode A.msg=NodeB.msg表示NodeA和NodeB有相同的初始化信息,并且它们能够互相通信。初始化模式中,表示NodeA必须知道NodeB的ID,NodeA和NodeB之间共享相同的密钥。操作Protocol定义了其中一个距离测定实现的整个过程。符号“∧”是Z语言中复合操作符。

VM表示一个可验证测距协议的执行过程,待验证者分别验证者发起距离界定请求,最终验证者将收到的距离信息发给中心节点,中心节点利用这些距离进行坐标计算,最终得到待验证者的位置信息。

4 无线传感器SPINE安全定位算法的形式化验证

我们已经前文中介绍了多点验证协议的形式化建模,接下来,我们将对其在无线传感器中的应用。由于信标节点大量部署代价昂贵,在大型传感器网络中,只需要部署少量信标节点,通过大量传感器间协作定位实现整个传感器网络的定位,我们可以选择一种合作定位机制称为SPINE(Secure Position for sensor NEtworks)算法。SPINE是基于VM安全定位机制的。SPINE通过验证至少三个锚节点的位置来估计未知节点的位置,估计出其他位置的未知节点会升级为锚节点,作为其它未知节点的参考节点。

在介绍SPINE算法之前首先介绍一种BDV(Basic Distance Verification)表示基本距离验证,它是利用VM机制进行距离界定的,u可以测量出duv,v可以测量出dvu。BDV界定u和v的距离过程如下:1)所有可验证v的三角形集合US,有△(u,v1,v2)、△(u,v1,v4)、△(u,v3,v4)、△(u,v2,v3);2)所有可验证u的三角形集合VS,有△(v,v5,v6)、△(v,v5,v6);3)所有可同时验证u和v的三角形集合UVS,有△(v4,v5,v6)。对于所有△l∈US∪VS∪UVS,可计算出dlvu=VM.Distance(u,v)以及dluv=VM.Distance(v,u),由此,对于所有△l∈US∪VS∪UVS,对于该节点执行δ测试和点再三角形内测试,对于通过测试的位置,就作为未知节点的定位结果,否则,就拒绝该位置,即只要|dluv-duv|<,且|dlvu-dvu|<δ,则{duv,dvu}的测量结果能够被接受。

SPINE算法执行过程如下:1)节点测量与邻居的距离;2)通过VM进行距离界定;3)所有节点间的互相定位采用分布式算法实现。定义集合VD=,表示可信任距离集合,初始为空;定义集合NV,表示所有未验证距离,初始为空;DB={所有距离集合}。那么对于所有dbi∈D B,如果dbi能够被B D V验证那么V D=V D∪{d bi},否则NV=NV∪{dbi}。

u和v的定位结果出来,有VD=VD∪{dbuv},同时u和v就成为验证节点,能够验证其他待验证节点,整个网络协同工作,直至整个定位过程完成。

我们已经可以对整个网络进行定位,但是,又是如何保证对整个定位过程是安全的?我们将展开简单的分析。如下图所示,图a是一个正常定位过程;图b中u对v进行距离扩大攻击,根据VM安全定位机制,能够检测出整个定位过程发生距离扩大攻击,抛弃本次定位结果;图c,同时三个入侵节点伪装同一个节点对定位发起攻击,根据VM算法本次攻击成功,定位被干扰。因此,当#VD>3(在object-z中,#表示集合个数)时,表示最少三个三角形同时对一个待验证节点发起验证,可防止如下图所示的各种扩大距离攻击。

4 结语

本文用形式化方法对无线传感器网络的安全定位进行了简单地分析,最后得出#VD>3时,可保证定位是准确且安全的。多点验证协议不仅可以用于无线传感器安全定位,还可以用于其他网络的安全定位,采用形式化方法对无线传感器网络进行安全定位分析在目前还属于少数,还有待继续深入研究。

参考文献

[1]H.A.Oliveira et al.,Directed position estimation:A recursivelocalization approach for wireless sensor networks,”14th IEEEInt’l.Conf.Comp.Commun.And Networks,San Diego,CA,Oct.2005,557 562.

[2]T.He et al.,Range-free localization schemes for large scalesensor networks,MobiCom’03:Proc.9th Annual Int’l.Conf.Mo-bile Comp.and Networking,New York:ACM Press,2003,81 95.

[3]J.Albowicz,A.Chen,and L.Zhang,Recursive position estimationin sensor networks,”9th Int’l.Conf.Network Protocols,Nov.2001,35 41.

[4]S.Brands and D.Chaum,Distance-bounding protocols,in Proc.Workshop on the theory and application of cryptographic tech-niques on ad-vances in cryptology,1994,pp.344 359.

[5]David A.C,David J.D Object-Z:An object-oriented extensionto Z,1989,Second International Conference on Formal Descrip-tion Techniques for Distributed Systems and Communication Pro-tocols 281 296.