检索结果-南通市图书馆

在线全文

学校读者我要写书评

暂无评论

约束求解与定理证明专题前言

软件学报 2023年第8期34卷 3465-3466页

作者：蔡少伟陈振邦王戟詹博华赵永望中国科学院软件研究所北京100190 国防科技大学计算机学院湖南长沙410073 浙江大学计算机科学与技术学院浙江杭州310007

随着计算机系统在工业和生活中越来越广泛的应用,软件和硬件的可靠性受到越来越多的关注.形式化方法使用严格的数学语言对计算机系统建模,并在计算机的辅助下验证系统的正确性.与测试不同,形式化方法可以完全排除某些类型的错误.约束求... 详细信息

随着计算机系统在工业和生活中越来越广泛的应用,软件和硬件的可靠性受到越来越多的关注.形式化方法使用严格的数学语言对计算机系统建模,并在计算机的辅助下验证系统的正确性.与测试不同,形式化方法可以完全排除某些类型的错误.约束求解和定理证明是形式化方法中的两大关键技术.在约束求解方面,SAT和SMT求解器已经在学术界和工业界得到了广泛应用,比如SAT求解器用于EDA领域的等价性验证,SMT求解器用于程序验证和白盒模糊测试等.交互式定理证明通过人和计算机之间的交互完成证明,能够验证非常复杂的系统和性质,例如编译器和操作系统的正确性验证.约束求解与定理证明专题关注约束求解和定理证明的理论、技术、工具与应用,包括在EDA、符号执行、模型检测、程序分析与验证、系统安全等领域的应用.

关键词：形式化方法定理证明约束求解符号执行计算机系统模糊测试模型检测系统安全

在线全文

学校读者我要写书评

暂无评论

定理证明理论与应用专题前言

软件学报 2022年第6期33卷 2113-2114页

作者：曹钦翔詹博华赵永望上海交通大学电子信息与电气工程学院上海200240 中国科学院软件研究所北京100190 浙江大学计算机科学与技术学院浙江杭州310027

随着计算机系统在工业和生活中越来越广泛的应用,软件和硬件的可靠性受到越来越多的关注.定理证明方法将程序和系统的正确性表达为数学命题,然后使用逻辑推导的方式证明正确性.不同于基于程序测试的技术,定理证明方法能保证覆盖所有边... 详细信息

随着计算机系统在工业和生活中越来越广泛的应用,软件和硬件的可靠性受到越来越多的关注.定理证明方法将程序和系统的正确性表达为数学命题,然后使用逻辑推导的方式证明正确性.不同于基于程序测试的技术,定理证明方法能保证覆盖所有边缘情况,完全排除一些特定类型的错误.而基于逻辑推导的交互式定理证明技术还能不受系统状态空间大小和复杂性的限制,验证非常复杂的系统和性质.因此,定理证明技术不仅是形式化方法领域,也是众多其他应用领域国内外学者的关注焦点和研究新热点.

关键词：逻辑推导定理证明形式化方法计算机系统数学命题程序测试关注焦点特定类型

基于精化的TrustZone多安全分区建模与形式化验证

在线全文

学校读者我要写书评

暂无评论

软件学报 2023年第8期34卷 3507-3526页

作者：曾凡浪常瑞许浩潘少平赵永望浙江大学计算机科学与技术学院浙江杭州310027 浙江大学杭州国际科创中心浙江杭州311200 浙江省区块链与网络空间治理重点实验室浙江杭州310027

TrustZone作为ARM处理器上的可信执行环境技术,为设备上安全敏感的程序和数据提供一个隔离的独立执行环境.然而,可信操作系统与所有可信应用运行在同一个可信环境中,任意组件上的漏洞被利用都会波及系统中的其他组件.虽然ARM提出了S-EL... 详细信息

TrustZone作为ARM处理器上的可信执行环境技术,为设备上安全敏感的程序和数据提供一个隔离的独立执行环境.然而,可信操作系统与所有可信应用运行在同一个可信环境中,任意组件上的漏洞被利用都会波及系统中的其他组件.虽然ARM提出了S-EL2虚拟化技术,支持在安全世界建立多个隔离分区来缓解这个问题,但实际分区管理器中仍可能存在分区间信息泄漏等安全威胁.当前的分区管理器设计及实现缺乏严格的数学证明来保证隔离分区的安全性.详细研究了ARM TrustZone多隔离分区架构,提出一种基于精化的TrustZone多安全分区建模与安全性分析方法,并基于定理证明器Isabelle/HOL完成了分区管理器的建模和形式化验证.首先,基于逐层精化的方法构建了多安全分区模型RMTEE,使用抽象状态机描述系统运行过程和安全策略要求,建立多安全分区的抽象模型并实例化实现分区管理器的具体模型,遵循FF-A规范在具体模型中实现了事件规约;其次,针对现有分区管理器设计无法满足信息流安全性验证的不足,设计了基于DAC的分区间通信访问控制,并将其应用到TrustZone安全分区管理器的建模与验证中;再次,证明了具体模型对抽象模型精化的正确性以及具体模型中事件规约的正确性和安全性,从而完成模型所述137个定义和201个定理的形式化证明(超过11000行Isabelle/HOL代码).结果表明:该模型满足机密性和完整性,并可有效防御分区的恶意攻击.

关键词：可信执行环境安全分区定理证明精化安全性分析

在线全文

学校读者我要写书评

暂无评论

基于时间抽象状态机的AADL模型验证

软件学报 2015年第2期26卷 202-222页

作者：杨志斌胡凯赵永望马殿富 Jean-Paul BODEVEIX Institut de Recherche en Informatique de Toulouse Université de Toulouse 北京航空航天大学计算机学院北京100191

提出了一种基于时间抽象状态机(timed abstract state machine,简称TASM)的AADL(architecture analysis and design language)模型验证方法.分别给出了AADL子集和TASM的抽象语法,并基于语义函数和类ML的元语言形式定义转换规则.在此基础... 详细信息

提出了一种基于时间抽象状态机(timed abstract state machine,简称TASM)的AADL(architecture analysis and design language)模型验证方法.分别给出了AADL子集和TASM的抽象语法,并基于语义函数和类ML的元语言形式定义转换规则.在此基础上,基于AADL开源建模环境OSATE(open source AADL tool environment)设计并实现了AADL模型验证与分析工具AADL2TASM,并基于航天器导航、制导与控制系统(guidance,navigation and control)进行了实例性验证.

关键词： AADL(architecture analysis and design language) TASM(timed abstract state machine) 模型转换形式验证

在线全文

学校读者我要写书评

暂无评论

遥感信息元数据集成服务系统的研究与实现

计算机应用 2006年第B6期26卷 285-287页

作者：潘志华赵永望胡春阳马殿富北京航空航天大学计算机新技术实验室北京100083

在SOA框架下研究遥感信息资源元数据的集成涉及的关键技术。系统中数据源以服务的方式动态接入,并通过一个中间代理层对外提供统一的服务;系统将W eb服务技术与联邦模式技术进行有机地结合,实现了异构遥感元数据的集成,支撑遥感数据的... 详细信息

在SOA框架下研究遥感信息资源元数据的集成涉及的关键技术。系统中数据源以服务的方式动态接入,并通过一个中间代理层对外提供统一的服务;系统将W eb服务技术与联邦模式技术进行有机地结合,实现了异构遥感元数据的集成,支撑遥感数据的跨域共享。试用结果表明,系统完全达到了设计目标,效果良好。

关键词： Web服务数据集成联邦模式遥感

基于黏菌优化算法与蒙特卡罗模拟的古滑坡体稳定性分析

在线全文

学校读者我要写书评

暂无评论

武汉科技大学学报 2024年

作者：曹昊钟冬望冯庆蔚何理赵永明李腾飞武汉科技大学冶金工业过程系统科学湖北省重点实验室武汉科技大学理学院中铁广州工程局集团港航工程有限公司

各类地质灾害的预防都离不开边坡稳定性的精准分析，本文依托重庆万州港临近古滑坡体水下炸礁爆破工程实践，考虑岩性参数的随机特征和爆破扰动因素，联合声波测试技术，提出基于黏菌智能优化算法和蒙特卡罗模拟的可靠度分析方法，对爆... 详细信息

各类地质灾害的预防都离不开边坡稳定性的精准分析，本文依托重庆万州港临近古滑坡体水下炸礁爆破工程实践，考虑岩性参数的随机特征和爆破扰动因素，联合声波测试技术，提出基于黏菌智能优化算法和蒙特卡罗模拟的可靠度分析方法，对爆区附近古滑坡体进行稳定性分析。结果表明：计算得到的古滑坡体稳定系数Fs为1.261，爆破前尚无失稳风险，且结果接近传统极限平衡法计算值；边坡的岩性随爆破次数增加而变化，前3次爆破对边坡的影响最大；最后受多次爆破扰动，边坡的稳定性系数从1.261下降至1.081，稳定系数降了14.2%。经过蒙特卡罗模拟，边坡失效概率平均为13.68%，边坡存在失稳风险，爆破扰动因素不可忽视，现场应进行边坡加固。该方法已成功应用于重庆万州疏浚炸礁项目，取得良好效果，可为同类工程提供参考。

关键词：边坡稳定性爆破扰动极限平衡法黏菌优化算法蒙特卡罗模拟

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

L4虚拟内存子系统的形式化验证

软件学报 2023年第8期34卷 3527-3548页

作者：章乐平赵永望王布阳李悦欣冯潇潇北京航空航天大学计算机学院北京100191 浙江大学网络空间安全学院浙江杭州310007 浙江大学移动终端安全技术浙江省工程研究中心浙江杭州310007

第二代微内核L4在灵活度和性能方面极大地弥补了第一代微内核的不足,这引起学术界和工业界的关注.内核是实现操作系统的基础组件,一旦出现错误,可能导致整个系统瘫痪,进一步对用户造成损失.因此,提高内核的正确性和可靠性至关重要.虚拟... 详细信息

第二代微内核L4在灵活度和性能方面极大地弥补了第一代微内核的不足,这引起学术界和工业界的关注.内核是实现操作系统的基础组件,一旦出现错误,可能导致整个系统瘫痪,进一步对用户造成损失.因此,提高内核的正确性和可靠性至关重要.虚拟内存子系统是实现L4内核的关键机制,聚焦于对该机制进行形式建模和验证.构建了L4虚拟内存子系统的形式模型,该模型涉及映射机制所有操作、地址空间所有管理操作以及带TLB的MMU行为等;形式化了功能正确性、功能安全和信息安全三方面的属性;通过部分正确性、不变式以及展开条件的推理,在定理证明器Isabelle/HOL中证明了提出的形式模型满足这些属性.在建模和验证过程中,发现源代码在功能正确性和信息安全方面共存在3点问题,给出了相应的解决方案或建议.

关键词： L4 形式化验证内存管理映射信息流安全 Isabelle/HOL

在线全文

学校读者我要写书评

暂无评论

系统软件构造与验证技术专题前言

软件学报 2020年第5期31卷 1241-1242页

作者：赵永望刘杨王戟北京航天航空大学计算机学院北京100191 School of Computer Science and Engineering Nanyang Technological UniversitySingapore 639798Singapore 国防科技大学计算机学院湖南长沙410073 高性能计算国家重点实验室(国防科技大学) 湖南长沙410073

系统软件是计算机系统的核心基础软件,涵盖基础系统软件,如操作系统、语言及编译器、中间件、数据库等;领域系统软件,如无人系统、工业控制、航空航天飞行器等的核心控制软件;人工智能系统软件和区块链关键基础软件等新型软件.系统软件... 详细信息

系统软件是计算机系统的核心基础软件,涵盖基础系统软件,如操作系统、语言及编译器、中间件、数据库等;领域系统软件,如无人系统、工业控制、航空航天飞行器等的核心控制软件;人工智能系统软件和区块链关键基础软件等新型软件.系统软件的安全可靠性关系到整个系统,如何构造并验证高质量的系统软件仍然是学术界和工业界面临的重大问题.尤其是系统软件构造与验证过程中,提高系统软件开发效率、提升系统软件质量、增强系统软件安全可靠性相关的理论与方法、技术与工具、应用与案例等,对于我国从事系统软件的研发人员,具有重要的参考价值.

关键词：软件开发效率计算机系统新型软件系统软件人工智能区块链中间件操作系统

爆破振动强度、波形与频谱研究综述：预测及主动控制

在线全文

学校读者我要写书评

暂无评论

爆破 2024年

作者：何理殷琳钟冬望张鑫玥赵永明熊海涛陈莎莎 NJAMBA Bruno 武汉科技大学冶金工业过程系统科学湖北省重点实验室江汉大学爆破工程湖北省重点实验室

岩石钻孔爆破不可避免的会产生爆破振动效应及危害，准确预测爆破振动效应并进行主动控制具有极大的现实意义。论文综述了近40年来，国内外研究人员在爆破振动预测及主动控制方面取得的研究成果。在爆破振动速度峰值（PPV）预测方面，... 详细信息

岩石钻孔爆破不可避免的会产生爆破振动效应及危害，准确预测爆破振动效应并进行主动控制具有极大的现实意义。论文综述了近40年来，国内外研究人员在爆破振动预测及主动控制方面取得的研究成果。在爆破振动速度峰值（PPV）预测方面，经验模型预测方法体现出了较大的便捷性，但预测精度与效果较差，将概率统计理论引入经验模型预测方法，提高了PPV预测精度；而基波叠加预测方法可实现对振速、频率和持续时间的综合预测，但是该方法对振动基波的测试精度要求较高，同时亟需在行业内建立对爆破振动采集设备的定期标定与校核机制；人工智能预测方法极大提高了PPV预测精度，同时为多因素影响下的爆破振动效应预测提供了新思路，但需要建立在海量真实有效实测数据的基础上，目前还缺乏充实的振动测试样本数据库；PPV预测理论模型及数值模拟预测法对理论与专业知识、数值模拟技术等要求高，限制了两种方法在工程的普遍应用。在爆破振动速度主动控制上，可以确定合理的延期时间，采用毫秒延迟干扰减振法来降低PPV，但目前多为单一防护对象所提出的延期时间建议值；从调整爆破振动频谱结构的角度，通过主动改变延期时间调控爆破振动频率成分，可避开建（构）筑物自振频带，减小爆破振动危害，然而目前仅仅停留在理论层面或模型试验尺度条件下，缺乏大规模的现场应用实例。最后，对未来爆破振动预测及控制方面重点研究内容进行了展望。

关键词：爆破振动基波叠加干扰减振频谱控制延期时间