摘要：虚拟化技术为安全关键系统提供了分区隔离等重要特性,虚拟机监视器(Virtual Machine Monitor,VMM)作为其核心组件,对客户系统的安全运行及虚拟机间威胁和故障的屏蔽起着决定性作用。文中从最小特权原则出发,将VMM的设计按是否与安全直接相关划分为内核扩展与用户进程,并采用分层精化的方法对内核扩展中的各关键模块展开了形式化建模与验证,继而以此为基础,证明了虚拟机实现的功能正确性。实验评估表明,原型系统的综合性能负载与主流虚拟化方案接近,安全划分的设计方法与形式化验证在提升VMM安全性的同时,并未对其产生明显负载,可较好地满足应用领域的需求。

摘要：针对软件开发中的一种软件验证技术———形式化验证技术进行研究,分析这种方法的原理和应用情况,并使用一个实例来说明这种方法在基于模型的软件开发中的使用方式,由这个过程可以看出,这种基于模型的形式化验证技术对于传统的软件验证方法来说是个有力的补充,对于一些高安全性的软件来说使用这种验证方式能有效提高软件的可靠性。

摘要：形式化验证是对传统验证方法的补充,是数字电路验证的一条有效途径,对于并发系统,行为建模是一种非常合适的建模方法;Rebeca是由Sirjani和Movaghar提出的一种基于行为的建模语言,支持形式化,一方面,Rebeca是一种类Java的语言,软件工程师很容易使用,另一方面,它是一种支持形式化验证及其相关理论的模型语言,可以为不精通于形式化方法的开发人员和研究人员提供方便的验证过程;在深入研究Rebeca的基础上,采用Rebeca对硬件设计进行建模,然后Modere形式化验证工具对AES密码芯片进行形式化验证。

摘要：Jourdan等在其2012年发表的论文“Validating LR(1)Parsers”中提出了一种形式化验证语法分析器的方法,并将其成功地应用于CompCert编译器(2.3以上版本)的语法分析器验证中。借助这种方法,文中完成了L2C项目中的Lustre*语言语法分析器的形式化验证,实现了开源L2C编译器前端语法分析器的两个选项之一。首先对这一语法分析器的实现进行了论述,其中包括有参考价值的技术细节;随后分析了该语法分析器的运行性能及正确性;最后对如何将这一方法推广至更一般的应用场景进行了总结。

摘要：为保证SCADE软件开发的安全性,研究了SCADE形式化验证技术,指出其不足,提出了基于代码生成器的解决方法。该方法对安全特性属性引入了逻辑描述,并利用SCADE编辑器及代码生成器的特点,对SCADE形式化验证技术进行改进,降低了模型正确性确认时人为的主观性。通过实例阐述了应用该方法进行形式化验证的一般步骤,表明了该方法是有效可行的。

摘要：空间总线(SpaceWire)协议是应用于航空航天领域的高速通信总线协议,保证其可靠性至关重要。但是由于通信系统具有队列量、分布控制和并发性等特点,传统仿真模拟的验证方法存在不完备性的问题,采用模型检测方法对高层次属性进行验证时,通常会出现状态爆炸的问题。基于xMAS模型对SpaceWire通信系统中的信誉逻辑进行形式化建模、验证,xMAS模型既保留了底层的结构信息,又可以验证高层次的属性。对通信系统中信誉逻辑进行抽象进而建立了xMAS模型,提取了可发送性、可接收性和数据一致性等3个关键属性,运用定理证明工具ACL2对关键属性的正确性进行了自动验证。该方法为验证指导下的系统设计提供了有效的参考。

摘要：通过对时态逻辑的研究来探讨时态逻辑在硬件设计形式化验证上的应用 ,同时对布尔函数在计算机内的表示二叉判定图 (BDD)进行了进一步地分析 。

摘要：为解决硬件电路形式化验证过程中,验证对象的结构过于庞大复杂难以进行形式化描述与验证的问题,提出一种结构建模法。对两种不同的结构建模方法 (分解法和迭代法)分别进行讨论,分析两种方法的异同点以及适用性,详述结构建模过程中需要用到的层次化技术和模块化技术。以超前进位产生器74LS182为例,详细分析验证对象的结构建模过程,给出结构建模前后验证对象的结构描述、验证流程等结果。通过对比结构建模前后验证对象的验证规模、难易程度和时间开销等,凸显了结构建模对硬件电路形式化验证过程的优化效应。

摘要：针对智能灌溉系统中嵌入式软件的可靠性,提出了在软件的设计阶段,采用MARTE建立软件的系统模型,通过将软件模型转换为形式化模型,对软件系统中各个子系统的可靠性进行验证。通过对智能灌溉系统的嵌入式软件进行可靠性分析,指出在本文假设前提下,数据采集单元软件的故障率最大,在实际应用中应该有针对性的进行改善,有助于解决不利于可靠性的影响因素,提高整个智能灌溉系统的可靠性。

摘要：针对模拟与混合信号(AMS)电路形式化建模逼真度低和描述不规范的问题,提出一种基于基尔霍夫电流定律节点分析的形式化建模方法。通过扩展计算树逻辑公式,在保留电路更多物理特性的前提下综合描述和验证AMS电路的离散事件和动态行为,保证性质验证的精确性和可信性。以环形振荡器为例,给出该方法的实现过程,并通过Coho工具对振荡器电路进行验证。实验结果表明该方法正确、有效。