【摘 要】
：
由于计算机技术在各个领域中的广泛应用,确保软件系统和硬件系统的正确性和可靠性显得非常关键。特别是在一些重要领域,例如航空航天、军事武器等,软硬件系统中的一个微小的错误可能会导致巨大的损失。在这些重要领域中,传统软件测试方法存在测试用例生成困难等缺点以致难以保证系统的可靠性,因此形式化验证方法作为传统软件测试方法的补充是保障系统可靠性的重要途径之一。其中基于时序逻辑的验证方法是形式化验证的方法之一,
论文部分内容阅读
由于计算机技术在各个领域中的广泛应用,确保软件系统和硬件系统的正确性和可靠性显得非常关键。特别是在一些重要领域,例如航空航天、军事武器等,软硬件系统中的一个微小的错误可能会导致巨大的损失。在这些重要领域中,传统软件测试方法存在测试用例生成困难等缺点以致难以保证系统的可靠性,因此形式化验证方法作为传统软件测试方法的补充是保障系统可靠性的重要途径之一。其中基于时序逻辑的验证方法是形式化验证的方法之一,并得到了广泛的应用。实验室基于PTL（Projection Temporal Logic）自主设计并研发了MSVL（Modeling,Simulation and Verification Language）程序设计语言。该语言具有建模、仿真及验证的功能。与此同时,实验室基于MSVL的理论,自主研发了MSVL解释器和MC（MSVL Compiler）工具。MC工具虽然提高了编译MSVL程序的速度,但是其内部的语义分析过程是非形式化的,因此违背了MSVL的设计初衷。本文主要研究了一个基于范式的MCⅡ（MSVL CompilerⅡ）的设计与实现,主要贡献如下:1.MCⅡ整体框架和模块功能的设计与实现。通过使用LLVM（Low Level Virtual Machine）工具进行MCⅡ的开发,LLVM中间表示IR（Intermediate Representatio n）作为MCⅡ的中间代码。围绕着MCⅡ的输入处理模块、预处理模块、词法语法分析模块、语义分析库模块、转换器模块、IR代码重组模块、后端模块以及错误处理模块进行了详细的介绍。其中,MCⅡ中最关键的是通过使用范式约简的方法确保语义分析库中的语义分析过程是形式化的。2.在IR层面对MCⅡ进行优化,详细地介绍了优化方案,通过程序示例,获取优化前、优化后的编译时间,并进行对比,证明该优化的有效性。3.解决了MCⅡ实现过程中遇到的关键问题,比如形式化语义分析的关键问题以及与系统平台相关的关键问题,对问题和解决方法都进行了详细的说明。4.使用MSVL语言编写矩阵乘法、求解四阶幻方和并行归并排序的示例程序,并对程序进行仿真,证明了MCⅡ的可用性以及实用性。
其他文献
随着微电子技术的不断发展,集成电路工艺水平的不断提高,芯片设计的难度和复杂度也在不断提升,设计的验证工作耗时逐渐超过设计本身。因此,芯片验证方法学的研究在学术界与工业界获得了更为广泛的关注,选择一种合适的芯片验证方法对于芯片团队开发效率的提升有着重要的意义。现有对于DUT的调试,只能通过插入动态探针和静态探针的形式以获取内部信号的信息。此方法需要占用额外的配件资源,并且灵活性不高。特别是对于静态探
功率VDMOSFET,以开关速度快、高输入阻抗、低驱动功率等优点而被广泛应用于开关电源、汽车电子、整流器等应用中,在电子电力系统中扮演着重要角色。而现阶段在高压VDMOS领域,国外已经有规模化的产线,而我国则处于起步阶段,该方面的需求主要依靠进口,存在采购周期长,价格高,且随时被禁运的风险。因此,使得能够自主研制出基于国内工艺产线,设计并生产的高压功率VDMOS器件对我国而言具有重要意义。本文的目
随着人工智能技术日益成熟,卷积神经网络（Convolutional Neural Network）作为最热门的机器学习算法之一,其应用范围逐步扩大,涉及生活中的方方面面,例如视频监控领域、无人驾驶和医疗器械等。在实际应用中,需要通过硬件平台加速神经网络的计算过程,建立高实时性、低功耗的可操作系统。现场可编程逻辑门阵列FPGA（Field Programmable Gate Array）作为一种包含
本文阐述某工业园区中途污水提升泵站系统改造和科学管理的方法与途径,以实际自动化升级改造、建立科学管理和优化运行模式案例为依据,证明其应用效果和实际价值,为相关污水提升泵站的系统与管理能力提升提供科学参考。
SLAM（同时定位与地图构建）是当下许多热门领域的基础技术,服务于自动驾驶、虚拟现实、增强现实在内的多个应用场景。利用搭载特定传感器的主体,SLAM技术可以在没有环境先验的前提下,于运动中进行场景三维重建,同时估计机器人自身位置和运动轨迹。然而,现有SLAM方法通常只适用于单机、单次作业,当场景规模逐渐扩大时,存在内存占用大、计算量高、轨迹漂移等问题,限制了在真实场景中的适用范围。为此,本文研究面
近年来,机器学习系统在社会各领域都有着广泛的应用。然而,由于其安全性和可靠性无法保证,在一些应用中可能造成重大的灾难,尤其在安全攸关系统中,一旦发生错误,其后果是无法接受的。形式化验证方法可以从数学的角度描述算法模型与期望性质,从而提高机器学习系统的安全性,不过系统的底层算法,如泰勒展开等,缺乏深入的形式化研究工作。命题投影时序逻辑PPTL（Propositional Projection Tem
计算机软件和硬件系统已经成为国民经济、人民生活和国防建设基础设施,但是系统的错误时有发生,因此如何保证软硬件系统的正确性、安全性和可靠性已成为一个重大挑战。然而,传统的软件测试方法已经无法完全保证计算机系统的可靠性、安全性和正确性。形式化验证方法在复杂的软硬件系统验证方面展现出极大的优势,受到越来越多的软硬件开发者的青睐。基于时序逻辑的验证方法作为形式化验证的主要流派受到了广泛的关注。实验室团队基
现代深度学习的成功很大程度上归功于海量数据的可用性。随着消费者对隐私问题越来越关注以及各国出台的隐私保护相关法案对个人数据的保护力度大幅增加,导致数据日益碎片化,形成了多个“数据孤岛”,成为了制约人工智能技术发展的瓶颈之一。作为一种支持数据隐私保护的分布式训练框架,联邦学习近年来受到了学术界和产业界的广泛关注,它旨在不交换训练数据的前提下进行协作训练,以此解决数据治理和隐私问题。尽管联邦学习的知名
泵站实现无人值守能有效解决人力资源消耗过高的问题，提高管理效能，是未来泵站发展的主要方向。目前中国无人值守泵站在具体发展过程中已经出现了使用自动化控制系统的例子，并且在实际应用的过程中能有效提高泵站的运行质量和效率，进而降低泵站的实际运营成本，为企业提高服务水平奠定坚实的基础。主要对无人值守泵站落实的基础条件、自控配置要求、视频监控联动以及远程操控的等方面进行了论述，在技术层面对无人值守泵站的构建
目的:考察童年期虐待经历对大学生情绪记忆的影响。方法:用儿童期虐待问卷中文版在大学生中筛出情感虐待伴忽视组23例，躯体虐待伴忽视组21例，对照组24例。实验1用3×3的混合实验设计；实验2用3×5的混合实验设计。结果:以情绪记忆的正确率为指标，实验1的效价主效应有统计学意义（P＜0.001）,负性图片高于正性图片和中性图片（均P＜0.001）,组别主效应有统计学意义（P＜0.05）,对照组高于两虐