检索结果-南通市图书馆

在线全文

学校读者我要写书评

暂无评论

形式化方法与应用专题前言

软件学报 2022年第8期33卷 2753-2754页

作者：陈立前孙猛国防科技大学计算机学院湖南长沙410073 北京大学数学科学学院北京100871

形式化方法基于严格的数学方法规约、设计、构建、验证、演进计算系统,是改善和保障计算系统可信性的重要方法.形式化方法相关基础理论、技术和工具已成功应用于各种软硬件系统的设计与验证.近年来,在区块链、深度学习、量子计算等新兴... 详细信息

形式化方法基于严格的数学方法规约、设计、构建、验证、演进计算系统,是改善和保障计算系统可信性的重要方法.形式化方法相关基础理论、技术和工具已成功应用于各种软硬件系统的设计与验证.近年来,在区块链、深度学习、量子计算等新兴领域,形式化方法也逐步应用适配,提升新兴领域计算系统的可信性.

关键词：形式化方法区块链软硬件系统深度学习量子计算数学方法可信性基础理论

在线全文

学校读者我要写书评

暂无评论

形式化方法概貌

软件学报 2019年第1期30卷 33-61页

作者：王戟詹乃军冯新宇刘志明国防科技大学计算机学院湖南长沙410073 高性能计算国家重点实验室(国防科技大学) 湖南长沙410073 中国科学院软件研究所北京100190 天基综合信息系统重点实验室(中国科学院软件研究所) 北京100190 南京大学计算机科学与技术系江苏南京210023 计算机软件新技术国家重点实验室(南京大学) 江苏南京210023 西南大学计算机与信息科学学院重庆400715 西南大学软件研究与创新中心重庆400715

形式化方法是基于严格数学基础,对计算机硬件和软件系统进行描述、开发和验证的技术.其数学基础建立在形式语言、语义和推理证明三位一体的形式逻辑系统之上.形式化方法已经以不同程度和不同方式愈来愈多地应用在计算系统生命周期的各... 详细信息

形式化方法是基于严格数学基础,对计算机硬件和软件系统进行描述、开发和验证的技术.其数学基础建立在形式语言、语义和推理证明三位一体的形式逻辑系统之上.形式化方法已经以不同程度和不同方式愈来愈多地应用在计算系统生命周期的各个阶段.介绍了形式化方法的发展历程和基本方法体系;以形式规约和形式验证为主线,综述了形式化方法的理论、方法、工具和应用的现状,展示了形式化方法与软件学科其他领域的交叉和融合;分析了形式化方法的启示,并展望了其面临的发展机遇和未来趋势.形式化方法的发展和研究现状表明:其应用已经取得了长足的进步,在提高计算系统的可靠性和安全性方面发挥了重要作用.在当今软件日益成为社会基础设施的时代,形式化方法将与人工智能、网络空间安全、量子计算、生物计算等领域和方向交叉融合,得到更加广阔的应用.研究和建立这种交叉融合的理论和方法不仅重要,而且具有挑战性.

关键词：形式化方法形式规约形式验证程序设计方法学软件开发

在线全文

学校读者我要写书评

暂无评论

形式化方法在电网信息物理系统中的应用

中国电力 2021年第3期54卷 31-37页

作者：黄莉梁云黄辉赵若涵全球能源互联网研究院有限公司北京102209 国家电网公司电力智能传感技术及应用联合实验室北京102209 国网电力科学研究院有限公司江苏南京210032

电网信息物理系统中的嵌入式终端不仅要具备常规的信息交互能力,还要在资源约束条件下,满足测控的实时性要求。面向规模庞大的复杂系统,需要引入形式化方法验证其可靠性。通过分析形式化方法在电网信息物理系统中的应用,设计实现一种适... 详细信息

电网信息物理系统中的嵌入式终端不仅要具备常规的信息交互能力,还要在资源约束条件下,满足测控的实时性要求。面向规模庞大的复杂系统,需要引入形式化方法验证其可靠性。通过分析形式化方法在电网信息物理系统中的应用,设计实现一种适用于电网信息物理系统中嵌入式系统信息交互过程分析的形式化方法及模型检验软件工具,并结合实际案例详细分析模型检验工具的应用过程。实际案例表明,形式化方法可以缩小从高层设计到代码实现的距离,提高产品的可靠性,模型检验软件工具能够对当前嵌入式装置规模和复杂度快速增长带来的可靠性保障问题提供可参考的解决方案。

关键词：电网信息物理系统形式化方法资源约束信息交互模型检验

基于形式化方法的DIMA动态重构仿真与验证

在线全文

学校读者我要写书评

暂无评论

系统工程与电子技术 2022年第4期44卷 1282-1290页

作者：刘嘉琛董磊赵长啸陈泓兵中国民航大学安全科学与工程学院天津300300 中国民航大学民航航空器适航审定技术重点实验室天津300300 天津市民用航空器适航与维修重点实验室天津300300

针对可重构分布式综合模块化航空电子(distributed integrated modular avionics,DIMA)系统在设计初期缺少仿真与验证手段的问题,首先分析了可重构DIMA软件体系的架构特征以及支持动态重构的层次化通用系统管理(generic system manageme... 详细信息

针对可重构分布式综合模块化航空电子(distributed integrated modular avionics,DIMA)系统在设计初期缺少仿真与验证手段的问题,首先分析了可重构DIMA软件体系的架构特征以及支持动态重构的层次化通用系统管理(generic system management,GSM)的组件功能划分。然后,使用架构分析与设计语言(architecture analysis and design language,AADL)及其相关附件对DIMA动态重构的架构基础、行为细节等要素进行建模。在此基础上,设计了一种基于形式化定义的模型转换规则,该规则将AADL动态重构模型转换成可执行的时间自动机模型。最后,利用模型验证工具UPPAAL验证了可重构DIMA系统逻辑及时序的正确性和不安全控制行为的可达性。结果表明,所提方法具有可行性和有效性,并且能够为后续DIMA动态重构的形式化安全性评估提供模型基础。

关键词：分布式综合模块化航空电子动态重构架构分析与设计语言形式化方法仿真验证

在线全文

学校读者我要写书评

暂无评论

基于形式化方法的平交道口控制系统安全设计

西南交通大学学报 2023年第1期58卷 109-116页

作者：王霞王恪铭徐扬唐伟健西南交通大学计算机与人工智能学院四川成都610031 西南交通大学系统可信性验证国家地方联合工程实验室四川成都610031 西南交通大学数学学院四川成都610031 西南交通大学信息科学与技术学院四川成都610031

铁路平交道口控制系统是一种典型的安全苛求系统,为提高铁路平交道口的安全性,提出一个能适应双线双向接车的自动控制系统.首先,分析现有铁路平交道口的作业流程,利用新的控制系统解决现有系统中常见的三个问题,即出清检查、制动距离限... 详细信息

铁路平交道口控制系统是一种典型的安全苛求系统,为提高铁路平交道口的安全性,提出一个能适应双线双向接车的自动控制系统.首先,分析现有铁路平交道口的作业流程,利用新的控制系统解决现有系统中常见的三个问题,即出清检查、制动距离限制、连续接车中防护门短时间开放问题;其次,基于Event-B语言以及精化策略对设计的自动控制系统建立形式化模型;最后,检查证明义务以验证需求属性是否被满足,并应用动画器Animation展示系统功能的正确性.结果显示:相比传统的道口管理系统,本文提出的自动控制系统增加了双线连续接车功能,且使用形式化建模和验证,避免系统设计中存在的二义性,对平交道口安全管理有一定的参考意义.

关键词：平交道口控制系统需求规范安全苛求系统形式化方法

在线全文

学校读者我要写书评

暂无评论

形式化方法与系统软件：实践与发展建议

前瞻科技 2023年第1期2卷 33-45页

作者：丁浩然王肇国付明陈海波上海交通大学软件学院华为德累斯顿研究所

对高可靠系统软件需求的不断增加使得形式化方法在工业界引起了广泛的兴趣。文章概述了当前主流形式化方法，分析了国内外研究态势，并介绍了形式化方法在设计和实现操作系统、编译器、同步原语、文件系统、数据库系统和分布式共识协议... 详细信息

对高可靠系统软件需求的不断增加使得形式化方法在工业界引起了广泛的兴趣。文章概述了当前主流形式化方法，分析了国内外研究态势，并介绍了形式化方法在设计和实现操作系统、编译器、同步原语、文件系统、数据库系统和分布式共识协议等方面的实践。基于这些实践，进一步总结了形式化方法在系统软件中应用的经验，并从理论和工程两方面讨论其可能面临的挑战，最后针对这些挑战提出发展建议。

关键词：形式化方法操作系统数据库文件系统分布式共识协议

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

形式化方法与应用专题前言

软件学报 2021年第6期32卷 1579-1580页

作者：田聪邓玉欣姜宇西安电子科技大学计算机学院陕西西安710071 华东师范大学软件学院上海200062 清华大学软件学院北京100084

计算机科学的发展主要涉及硬件和软件的发展,而软、硬件发展的核心问题之一是如何保证它们是安全可靠的.如今,硬件性能变得越来越高,运算速度也越来越快,体系结构、软件的功能也更加复杂,如何开发可靠的软、硬件系统,是计算机科学发展... 详细信息

计算机科学的发展主要涉及硬件和软件的发展,而软、硬件发展的核心问题之一是如何保证它们是安全可靠的.如今,硬件性能变得越来越高,运算速度也越来越快,体系结构、软件的功能也更加复杂,如何开发可靠的软、硬件系统,是计算机科学发展面临的巨大挑战.特别是现在计算机系统广泛应用于许多安全攸关系统中,如高速列车控制系统、航空航天控制系统、医疗设备控制系统等等,这些系统中的错误可能导致灾难性后果.

关键词：形式化方法计算机科学计算机系统运算速度硬件性能控制系统体系结构硬件系统

在线全文

学校读者我要写书评

暂无评论

形式化方法类课程设置及教学内容探索

计算机教育 2022年第6期 213-216页

作者：华保健樊淇梁潘志中中国科学技术大学软件学院江苏苏州215123

分析目前计算机和软件工程专业形式化方法类课程的现状,并根据软件工程发展形势的最新要求以及课程体系与ACM/IEEE CS2013计算机科学课程体系规范中知识主体的对应关系,指出现行课程体系的可改进之处,阐述重新构建形式化方法类课程体系... 详细信息

分析目前计算机和软件工程专业形式化方法类课程的现状,并根据软件工程发展形势的最新要求以及课程体系与ACM/IEEE CS2013计算机科学课程体系规范中知识主体的对应关系,指出现行课程体系的可改进之处,阐述重新构建形式化方法类课程体系的可行途径.

关键词：形式化方法编程语言软件可靠性

在线全文

学校读者我要写书评

暂无评论

基于形式化方法的智能合约验证研究综述

网络与信息安全学报 2022年第4期8卷 12-28页

作者：张文博陈思敏魏立斐宋巍黄冬梅上海海洋大学信息学院上海201306 上海市高可信计算重点实验室上海200062 上海电力大学上海201306

智能合约是区块链技术应用的一个重要场景,智能合约技术实现了区块链的可编程化,提高了其扩展性,有广阔的应用前景。然而,一系列关于智能合约的安全事件造成了大量经济损失,削弱了人们的信心,安全性问题已经成为制约智能合约进一步发展... 详细信息

智能合约是区块链技术应用的一个重要场景,智能合约技术实现了区块链的可编程化,提高了其扩展性,有广阔的应用前景。然而,一系列关于智能合约的安全事件造成了大量经济损失,削弱了人们的信心,安全性问题已经成为制约智能合约进一步发展的关键问题。如果合约设计和代码实现的过程中存在缺陷,可能会造成严重后果。而智能合约发布后无法修改,因此,在智能合约发布前对其正确性做出验证尤为重要。近年来,国内外学者在智能合约的验证领域取得了大量成果,但对这些研究成果的系统分析和总结相对较少。对以太坊的交易过程、gas机制、存储结构、编写语言做了简要介绍,在此基础上调查归纳了智能合约中常见的8种漏洞类型,解释了漏洞产生的原因,回顾了一些真实发生的安全事件并给出了漏洞示例代码;根据不同的技术手段,如符号执行、模型检测、定理证明等,对智能合约的形式化验证工作做分类介绍,分析了各种方法的优劣,并选取了3个开源的自动化验证工具Mythril、Slither和Oyente,从运行效率、检测漏洞类型以及准确率等方面作出实验评估和对比;研究了目前已有的相关综述文章,总结了这些研究的区别与优势;概述了智能合约的漏洞检测技术中仍存在的关键问题,对智能合约验证工作的现状进行了分析和展望,提出了未来能够进一步研究的方向。

关键词：智能合约形式化方法区块链以太坊程序验证