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



Abstract:



PDF全文下载地址:

http://jos.org.cn/jos/article/pdf/6256