摘要:安全案例提供清晰、全面和可靠的论据, 说明系统在特定环境下的操作满足可接受的安全性. 在受监管的安全攸关领域, 如汽车、航空和核能等领域, 认证机构通常要求系统经过严格的安全评估程序, 以确保其符合一个或多个安全标准. 在系统开发中应用安全案例是一种新兴的技术手段, 以结构化和全面的方式表达安全攸关系统的安全属性. 对安全案例的4个基本构建步骤: 确定目标、收集证据、构建论证和评估安全案例, 进行简要介绍. 然后聚焦于构建论证这一关键步骤, 详细介绍现有的8种安全案例表达形式, 包括目标结构符号(GSN)、声明-论点-证据(CAE)、结构化安全案例元模型(SACM)等, 并分析了它们的优缺点. 由于安全案例所需材料的显著复杂性, 软件工具通常被用作构建和评估安全案例的实用方法. 比较7种用于安全案例开发和评估的工具, 包括astah system safety、gsn2x、NOR-STA、Socrates、ASCE、D-Case Editor和AdvoCATE. 此外, 还深入探讨了安全案例构建中所面临的多重挑战, 这些挑战包括数据的可靠性和完整性、复杂性和不确定性的管理、监管和标准的不一致、人因工程、技术的快速发展以及团队和跨学科合作6个方面. 最后, 展望安全案例的未来研究方向, 揭示其潜在应用和研究问题.

摘要:概率程序将概率推理模型与图灵完备的编程语言相结合，统一了对计算和不确定性知识的形式化描述，能够有效地处理复杂的关系模型和不确定性问题.提供了一种用于分析仿射概率程序的工具PROPER.一方面，它有助于定性和定量地分析仿射概率程序的终止性，可以验证该概率程序是否以概率1终止，估计期望终止时间的上限，并计算步数N，使得N步后给定程序的终止概率呈指数下降；另一方面，它可以估计一个断言成立的概率区间，这有助于分析变量不确定性对概率程序结果的影响.通过实验表明，PROPER对分析各种仿射概率程序是有效的.

摘要:计算机科学的发展主要涉及硬件和软件的发展，而软、硬件发展的核心问题之一是如何保证它们是安全可靠的。如今，硬件性能变得越来越高，运算速度变得越来越快，体系结构变得越来越复杂，软件的功能也变得越来越复杂，如何开发可靠的软、硬件系统，己经成为计算机科学发展的巨大挑战。特别是现在计算机系统广泛应用于许多安全攸关系统中，如高速列车控制系统、航空航天控制系统、核反应堆控制系统、医疗设备控制系统等等，这些系统中的任何错误都可能导致灾难性后果。形式化方法己经成功应用于各种硬件设计，特别是芯片的设计。各大硬件制造商都有一个非常强大的形式化方法团队为保障系统的可靠性提供技术支持，例如IBM、AMD等等。近年来，随着形式验证技术和工具的发展，特别是在程序验证中的成功应用，形式化方法在处理软件开发复杂性和提高软件可靠性方面已显示出无可取代的潜力。各个著名的研究机构都投入了大量人力和物力从事这方面的研究。例如，美国宇航局NASA拥有一支庞大的形式化方法研究团队，他们在保证美国航天器控制软件正确性方面发挥了巨大作用，在美国研发“好奇号”火星探测器时，为了提高控制软件的可靠性和生产率，广泛使用了形式化方法。在新兴领域，如区块链及人工智能等领域，形式化方法也逐步得到应用，提升系统的整体安全可控。本专题公开征文，共征得投稿27篇。特约编辑先后邀请了国内外在该领域比较活跃的学者参与审稿工作，每篇投稿至少邀请2位专家进行初审。大部分稿件经过初审和复审两轮评审，部分稿件经过了两轮复审。通过初审的稿件还在FMAC 2020大会上进行了现场报告，作者现场回答了与会者的问题，并听取了与会者的修改建议。最终有18篇论文入选本专题。

摘要:Paxos是一个在不可靠的分布式处理器网络中解决共识问题的算法族.共识问题是指分布式系统中一组参与者就一个结果达成一致的过程.随着Paxos在大型分布式系统中的广泛运用，比如区块链系统以及谷歌文件系统等，其安全性证明越来越重要.在定理证明工具Coq中，形式化描述和定义了Lamport的Basic Paxos算法，并且证明了其满足共识性.

摘要:互模拟是并发系统分析和验证的一个重要概念.主要扩展了一种由Du和Deng提出的准局部算法，使其更加适用于一般的标记迁移系统.用Java实现扩展后的准局部算法与Fernandez和Mounier提出的局部算法.以VLTS为实验数据基准进行大量的实验，发现在大多数情况下，前者的性能比后者更好.同时，修改了算法使其能够验证模拟关系.最后，用Java实现对标记迁移系统进行转换，使算法同时可以验证弱互模拟关系.