形式化验证相关论文
因通信的同步问题、网络分区的可靠性问题等，分布式系统难以在通信、分区等环节失效的情况下对特定的状态达成共识．Paxos是近年分布......
区块链技术是当今正快速崛起的一门新兴技术,在数字金融、电子存证等关键敏感领域中具有强大的应用潜力,它在国家信息技术创新领域......
实时系统的建模与验证是实时系统开发过程中不可或缺的环节。由于目前业界中广泛使用的建模验证工具UPPAAL存在下载安装慢、拖拽控......
本文面向适航标准DO-331和DO-333,提出了一种机载软件分层精化开发和验证方法,形成了一套完整的软件开发和验证流程。本方法开发过......
PLC是工业控制领域中广泛应用的可编程逻辑控制器,在安全攸关的领域,传统的手工编程方式无法保证PLC程序的正确性,而在代码自动生......
在航空发动机全权限数字电子控制(FADEC)软件研制过程中,可重用基准模型库的开发和使用是提升软件研发效率和质量的重要技术手段.......
随着区块链和智能合约技术的广泛运用,越来越多的数字资产、隐私信息等敏感数据被存储到区块链上,因此区块链应用中的安全漏洞可能......
结构分析描述语言(AADL)是一种描述任务关键嵌入式系统架构和行为的建模语言,在航空航天领域广泛被应用.为验证AADL模型的任务关键......
自动驾驶场景中存在着丰富的时空数据和动态行为交互,使得自动驾驶场景充满复杂性。系统的安全性面临着严重的挑战。近年来,人们尝......
随着人工智能、机器人技术的不断发展和变革,机器人正逐渐进入人类生产生活的各个领域,机器人操作系统（Robot Operating System,ROS......
人工智能已在社会各行业得到了广泛应用,如人脸识别、自动驾驶、智慧医疗等。机器学习是实现人工智能的重要途径,相关系统在安全攸......
区域覆盖算法广泛用于群机器人解决资源勘查、目标搜救、地形测绘等问题.目前,对区域覆盖算法的研究主要是用传统计算机仿真和数值......
验证是FPGA开发流程和IC芯片设计流程中不可或缺的环节,文章首先分析了当前数字仿真验证用例设计无法跨越的不完备性和不充分性,并......
根据联锁系统的形式化验证系统需求,设计一种联锁数据翻译器软件的总体方案,实现站点接口文件、TLE文件和布尔逻辑文件等文件的翻......
针对代币智能合约的形式化验证方法中模型检测存在的状态空间爆炸问题,提出了一种两段式模型检测方法.使用图转换规则对智能合约建......
核电站控制保护逻辑规模庞大、逻辑复杂,通常采用面向工程人员的图形语言开发,并自动生成C代码实现。如何保证图形语言到C代码转换......
MSVL（Modeling,Simulation and Verification Language）是一种时序逻辑程序设计语言,是投影时序逻辑（Projection Temporal Logic,PTL）......
形式化软件方法采用数学的方法对软件进行建模和验证,可提高软件安全性.本章讨论了软件的形式化开发方法,讨论了形式化验证的问题,......
对机器人控制算法进行验证工作,对于保障机器人安全工作具有重要意义.本文给出了一个可以在双臂机器人无碰撞运动规划中应用的空间......
随着传感网络以及嵌入式系统等的发展，集计算、通信、控制于一体的信息CPS逐渐成为人们关注的热点。未来CPS将会应用到社会生活的各......
文章给出一个通用的针对复杂功能部件的形式化验证方法.该方法基于寄存器传输级设计，利用设计中的结构信息将电路划分为控制部分和......
线性命题时态逻辑（LPTL）可定性地描述系统的时间特性，自动机可用于计算机系统的建模。LPTL与自动机之间有着紧密的联系。结合LPTL语义......
IEEE属性描述语言PSL为描述硬件设计的属性提供了一种标准语言,基于断言的验证方法(ABV)为硬件的设计和验证提出了一种新的很具有......
针对嵌入式控制系统中的时序安全问题,提出一种形式化验证方法,使用证明助手Coq对嵌入式控制系统建模,并验证其时序安全性质.首先,......
介绍操作系统验证理论、语言和工具等技术基础,阐述验证路径、精化关系验证和大规模验证等新的验证方法和理念。比较分析多个操作......
以太坊智能合约是区块链技术的典型应用和实现。由于智能合约一旦部署就难以修改,智能合约在上链之前的正确性显得至关重要。虽然......
近年来,Web服务作为一种基于XML和HTTPS的一种服务,已经普遍被学术界和工业界所重视。Web服务组合具有动态与适应性、层次性和课扩......
摄动开普勒问题广泛应用于卫星轨道摄动分析,然而卫星轨道摄动分析数学模型的错误将导致灾难性后果.传统的建模与分析方法涉及到矢......
联调联试是高铁信号系统开通运营前的最后测试验证环节,意义重大。通过分析联调联试技术现状与挑战,针对传统黑盒测试等方法的局限......
随着Web服务技术的发展，服务的数量不断增加，然而网络上注册的大部分Web服务都是功能单一、结构简单的服务，当面对用户提出复杂的服务......
作为计算机软件的核心,操作系统的安全对于所有的计算机软件来说都至关重要。但是由于操作系统的规模非常庞大,而且结构极其复杂,......
SystemC是一种软硬件协同设计语言，可以完成从系统级(System Level)到寄存器传输级(Register Transfer Level，RTL)的设计。相比软硬......
操作系统是整个计算机系统的基础,它的可靠性、安全性影响到整个系统的可靠性、安全性。操作系统中最重要的部分是系统内核,因此必......
数字电路形式化验证通常有三种方法:定理证明、模型检验和等价性检验.这些方法都是利用数学机制来验证数字电路的性质.在工业界中,......
由于片上系统(SoC)的规模和功能在不断膨胀,为了保证设计的正确性,缩短设计的周期,在设计过程中的验证就变得越来越重要,也更为复......
在芯片的设计流程中,一般采用多种验证手段来确保芯片的正确性,包括功能验证,时序验证,测试验证等.其中最耗时的当推是功能验证,它......
随着信息技术的不断发展，软件系统的正确性越来越得到人们的关注。程序验证是保证软件系统正确性的一个重要手段。大多数人的关注点......
安全操作系统的设计和实现过程中对形式化方法有很高的要求。在各种形式化验证方法中，模型检验以其自动化程度高并且能够提供验证反......
随着软件产业的迅速发展，软件系统的功能和结构日益复杂，人们对于软件产品的质量要求也越来越高。最常用的程序质量问题检测的技术包......
大量的硬件和软件系统广泛应用在一些重要的领域，在许多情况下错误和失效是不可接受的。需要提供方法来检验软硬件的正确性，增强我们......
判定两个进程是否具有某种等价关系，是形式化验证的重要组成部分，很多种等价关系被定义出来以满足不同的验证需求，强互模拟等价和分支......
形式化验证主要是通过精确的分析来证明或证伪硬件或软件系统中一些明确的声明或者性质。形式化验证方法在广义上可以分成两大类：模......
如何保证软件系统的正确性一直是人们所关注的问题，为了能够准确、快速地找到软件系统中存在的问题，研究者们研发出了对软件系统进行......
