首页 | 本学科首页   官方微博 | 高级检索  
文章检索
  按 检索   检索词:      
出版年份:   被引次数:   他引次数: 提示:输入*表示无穷大
  收费全文   1篇
  免费   0篇
  国内免费   5篇
自动化技术   6篇
  2024年   1篇
  2022年   1篇
  2021年   1篇
  2020年   1篇
  2019年   1篇
  2018年   1篇
排序方式: 共有6条查询结果,搜索用时 0 毫秒
1
1.
田聪  邓玉欣  姜宇 《软件学报》2021,32(6):1579-1580
计算机科学的发展主要涉及硬件和软件的发展,而软、硬件发展的核心问题之一是如何保证它们是安全可靠的。如今,硬件性能变得越来越高,运算速度变得越来越快,体系结构变得越来越复杂,软件的功能也变得越来越复杂,如何开发可靠的软、硬件系统,己经成为计算机科学发展的巨大挑战。特别是现在计算机系统广泛应用于许多安全攸关系统中,如高速列车控制系统、航空航天控制系统、核反应堆控制系统、医疗设备控制系统等等,这些系统中的任何错误都可能导致灾难性后果。 形式化方法己经成功应用于各种硬件设计,特别是芯片的设计。各大硬件制造商都有一个非常强大的形式化方法团队为保障系统的可靠性提供技术支持,例如IBM、AMD等等。近年来,随着形式验证技术和工具的发展,特别是在程序验证中的成功应用,形式化方法在处理软件开发复杂性和提高软件可靠性方面已显示出无可取代的潜力。各个著名的研究机构都投入了大量人力和物力从事这方面的研究。例如,美国宇航局NASA拥有一支庞大的形式化方法研究团队,他们在保证美国航天器控制软件正确性方面发挥了巨大作用,在美国研发“好奇号”火星探测器时,为了提高控制软件的可靠性和生产率,广泛使用了形式化方法。在新兴领域,如区块链及人工智能等领域,形式化方法也逐步得到应用,提升系统的整体安全可控。 本专题公开征文,共征得投稿27篇。特约编辑先后邀请了国内外在该领域比较活跃的学者参与审稿工作,每篇投稿至少邀请2位专家进行初审。大部分稿件经过初审和复审两轮评审,部分稿件经过了两轮复审。通过初审的稿件还在FMAC 2020大会上进行了现场报告,作者现场回答了与会者的问题,并听取了与会者的修改建议。最终有18篇论文入选本专题。  相似文献   
2.
安全案例提供清晰、全面和可靠的论据,说明系统在特定环境下的操作满足可接受的安全性.在受监管的安全攸关领域,如汽车、航空和核能等领域,认证机构通常要求系统经过严格的安全评估程序,以确保其符合一个或多个安全标准.在系统开发中应用安全案例是一种新兴的技术手段,以结构化和全面的方式表达安全攸关系统的安全属性.我们对安全案例的四个基本构建步骤—确定目标、收集证据、构建论证和评估安全案例—进行简要介绍.然后聚焦于构建论证这一关键步骤,详细介绍现有的8种安全案例表达形式,包括目标结构符号(GSN)、声明-论点-证据(CAE)、结构化安全案例元模型(SACM)等,并分析了它们的优缺点.由于安全案例所需材料的显著复杂性,软件工具通常被用作构建和评估安全案例的实用方法.我们比较7种用于安全案例开发和评估的工具,包括Astah System Safety、gsn2x、NOR-STA、Socrates、ASCE、D-Case Editor和AdvoCATE.此外,本文还深入探讨了安全案例构建中所面临的多重挑战,这些挑战包括数据的可靠性和完整性、复杂性和不确定性的管理、监管和标准的不一致、人因工程、技术的快速发展以及团队和跨学科合作6个方面.最后,我们展望安全案例的未来研究方向,揭示其潜在应用和研究问题.  相似文献   
3.
郑晓琳  邓玉欣  付辰  雷国庆 《软件学报》2018,29(6):1517-1526
互模拟是并发系统的分析和验证的一个重要概念。本文主要扩展了一种由Du和Deng提出的准局部算法,使其更加适用于一般的标记迁移系统。我们用Java实现扩展后的准局部算法与Fernandez和Mounier提出的局部算法。我们以VLTS为实验数据基准,进行大量的实验,发现在大多数情况下,前者的性能比后者更好。同时,我们修改了算法使其能够验证模拟关系。最后,我们用Java实现对标记迁移系统进行转换,使算法同时可以验证弱互模拟关系。  相似文献   
4.
赵旭慧  邓玉欣  符鸿飞 《软件学报》2022,33(12):4464-4475
概率程序将概率推理模型与图灵完备的编程语言相结合,统一了对计算和不确定性知识的形式化描述,能够有效地处理复杂的关系模型和不确定性问题.提供了一种用于分析仿射概率程序的工具PROPER.一方面,它有助于定性和定量地分析仿射概率程序的终止性,可以验证该概率程序是否以概率1终止,估计期望终止时间的上限,并计算步数N,使得N步后给定程序的终止概率呈指数下降;另一方面,它可以估计一个断言成立的概率区间,这有助于分析变量不确定性对概率程序结果的影响.通过实验表明,PROPER对分析各种仿射概率程序是有效的.  相似文献   
5.
李亚男  邓玉欣  刘静 《软件学报》2020,31(8):2362-2374
Paxos是一个在不可靠的分布式处理器网络中解决共识问题的算法族.共识问题是指分布式系统中一组参与者就一个结果达成一致的过程.随着Paxos在大型分布式系统中的广泛运用,比如区块链系统以及谷歌文件系统等,其安全性证明越来越重要.本文在定理证明工具Coq中形式化描述和定义了Lamport的Basic Paxos算法,并且证明了其满足共识性.  相似文献   
6.
介绍一个可在经典计算机上模拟量子计算的工具Qsimulation。该工具由4个主要部分组成:一个命令式的量子编程语言,一个量子计算解释器,一个用于模拟量子程序执行的图形用户界面以及错误处理模块,它能帮助教师和新手设计并测试简单的量子电路和量子程序。  相似文献   
1
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号