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

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

SOC的形式化验证方法

针对SOC验证的需要,研究了形式化验证方法,重点分析了二元决策图(BDD)的等效性检查技术,设计了FSM等效性检查的程序,以及算法级描述控制流程到BDD转换方法;研究了利用计算树逻辑进行的模型检查技术,给出了CTL模型检查的处理流程;提出了形式化仿真的模型以及测试向量生成算法.     

SOC的形式化验证方法

如何对片上系统(SOC)来进行验证,是一个比较复杂的问题。本文介绍了用形式化方法来验证SOC,讨论在对SOC进行等价性验证时应注意的几个问题以及解决的方法。最后给出了对SOC验证的一般方法。     

基于CSP的形式化方法研究

CSP(通讯顺序进程)和B方法都是一种较好的用于实时控制系统构架分析的形式化方法,但是单独一种在描述实时控制系统构架时都存在不足.通过对CSP技术和B方法的研究,提出了一种能够描述分布式系统和实时控制系统的形式化方法-CSP-B,CSP-B集成了CSP技术和B方法,不仅具有CSP技术的特点,而且还有B方法的长处,并将CSP-B运用到证券分配系统中.     

形式化方法(FM)

传统的开发方法一般基于自然语言的描述,不能表达明确的语义;本文介绍的形式化方法（ＦＭ）是基于形式逻辑和离散数学的,特别适用于安全重要性系统的说明、设计和构造。     

基于TrustZone的TEE设计与信息流形式化验证

基于可信硬件构建安全关键应用的可信执行环境（TEE）,是嵌入式安全领域的一个研究热点。虽然底层硬件可信,但TEE软件仍可能因错误使用硬件指令或存在其他安全漏洞而导致机密信息泄露。该文基于ARM TrustZone技术提出了多层次的TEE架构,并建立了安全通信通道,用户层可信应用不能直接访问非可信环境的软硬件资源,只能通过内核层的安全通信通道API与外界通信,因此整个TEE的信息流不再受用户层影响。该文进一步提出了TEE形式化模型（TEEFM）,借助Coq辅助证明器验证了TEE信息流无干扰性并证明了TEE安全监控模块不存在整型溢出、程序返回地址异常等资源边界类软件漏洞,以此保证了TEE的自身安全性。     

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

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

混合系统的最优镇定

本文将文献[1]中用于离散系统的最优镇定定理推广到由离散系统和分布参数系统组成的混合系统,并讨论了由刚体和弹性体组成的受控混合系统的最优镇定问题。     

针对硬件木马的形式化验证模型构造方法

针对硬件安全验证的效率受形式化验证模型构建方式影响的问题,提出了一种面向硬件木马检测的自动构造形式化验证模型的方法.该方法首先遍历寄存器传输级设计的控制流图,提取出赋值语句的路径条件及其对应赋值表达式,构成Kripke结构中状态转移的约束关系;然后将Verilog语法的约束关系转换成模型检测器的语法,从而生成形式化验证...     

基于Event-B的形式化建模关键技术研究

软件系统的规模和复杂程度不断提高而传统的需求分析方法难以确保软件的正确性和一致性,为软件系统的质量埋下了隐患. 软件工程的实践表明,在开发过程中,错误发现得越早,修复得越早,付出的代价越小. 为了确保软件的质量,可在软件开发的早期需求分析阶段,采用Event-B形式化方法描述软件的需求,并验证模型的正确性. 以文件系统建模为例,该文讨论了如何利用Event-B方法,采用逐步精化的方式建立并验证模型,确保软件的正确性.     

带有二阶导数的混合块方法

本文讨论了一类求解常微分方程初值问题的带有二阶导数项的混合块方法。首先讨论了这类方法的一些一般性质,得到了方法收敛的一些条件;然后讨论了方法所能达到的阶数为3k+3;最后指出当k≤2时方法是A-稳定的,并给出了几个数值例子。     

带有二阶导数的混合块方法

本文讨论了一类求解常微分方程初值问题的带有二阶导数项的混合块方法。首先讨论了这类方法的一些一般性质,得到了方法收敛的一些条件;然后讨论了方法所能达到的阶数为3k 3;最后指出当k≤2时方法是 A 稳定的,并给出了几个数值例子。     

形式显示的方法与海德格尔思想的主题

海德格尔的思想是一个有机的整体性思想,在＂思想的事情的规定＂为特点的形式显示的方法指引下,海德格尔从此在的＂在-世界中-存在＂到存在的历史再到语言的沉默,一步步地追问出本真意义上的存在自身来。     

磁悬浮式驱动提花织针的控制策略与实验方法

本文针对针织提花圆纬机的工作原理,提出了一种磁悬浮式驱动织针模型。该模型以电磁、永磁混合原理为基础,通过对该模型进行实验分析和控制策略以及算法研究,验证了磁悬浮驱动织针在狭小空间内运动的可行性;同时对实验数据进行分析,进而验证理论的正确性。文中将单织针控制原理扩展延伸到多织针控制系统,并对多悬浮式驱动织针控制策略进行了探讨。     

线性哈密尔顿系统的m次连续有限元法

利用常微分方程的连续有限元法证明了m次连续有限元算法能保持哈密尔顿系统的能量守恒。对线性哈密尔顿系统的m次连续有限元算法为辛算法,且能保持能量守恒,数值例子也验证了此结论。     

线性哈密尔顿系统的m次连续有限元法

利用常微分方程的连续有限元法证明了m次连续有限元算法能保持哈密尔顿系统的能量守恒。对线性哈密尔顿系统的m次连续有限元算法为辛算法，且能保持能量守恒，数值例子也验证了此结论。     

论"形式对等"作为现代、后现代诗歌翻译之策略

文章主要探讨“形式对等”在现代与后现代诗歌翻译中的适用性。通过对肯明斯的诗作“In Just”的两个译本的比较和分析，从现代与后现代诗歌的特点和形式主义的角度，重新剖析“形式对等”这一翻译原则对于现代与后现代诗歌翻译的有效性及其在翻译理论中的发展。     

战略信息系统规划群决策支持系统框架分析

战略信息系统规划(SISP)是当前企业界和学术界共同关注的主题。为了适应日益激烈的市场竞争与复杂多变的动态环境,提高SISP的效果及其规划速度,采用规范研究方法,设计了一个SISP的群决策支持系统(SISPGDSS)的总体框架结构。该框架强调环境扫描,根据扫描结果选择不同的规划策略,以人为中心,为决策者创造一个智能的人机交互和互相交流的环境,根据SISP过程的各个阶段,选择不同的SISP方法。     

基于混合神经网络编队协同空战决策支持系统

针对缺少先验知识的前提下,提出一种混合神经网络编队协同空战决策支持系统,同时采用一种无教师一有教师的混合训练算法来训练混合神经网络。仿真结果表明该系统的有效性。